Lean/Mathlib: x ^ (1/2) is x ^ 0 = 1 for real x; write (1/2 : ℝ) or use √x

For x : ℝ, the exponent in x ^ (1/2) elaborates as a natural number, and ℕ division truncates, so 1/2 = 0. On Mathlib v4.35.0, example (x : ℝ) : x ^ (1/2) = 1 := by norm_num compiles. A 'square root' written this way silently turns into a theorem about 1, and later proofs either become trivial or fail mysteriously. Write x ^ (1/2 : ℝ) (rpow) or, better, Real.sqrt x / √x; the bridge between them is Real.sqrt_eq_rpow : √x = x ^ (1/2 : ℝ). The same trap applies to any fractional literal exponent like (2/3). Separately, the old big-operator syntax ∑ i in s, f i is now a parse error ('unexpected token in; expected ,'), so write ∑ i ∈ s, f i.