R : Type u
⊢ Real.sqrt 2 ^ 4 = Real.sqrt 2 * (Real.sqrt 2)⁻¹ * 4
R : Type u
⊢ Real.sqrt 2 * Real.sqrt 2 ^ 3 = Real.sqrt 2 * (2 * (Real.sqrt 2)⁻¹ + 4 * ((Real.sqrt 2)⁻¹ * 2⁻¹))
ring_nf
R : Type u
⊢ Real.sqrt 2 ^ 4 = 1 * 4
R : Type u
⊢ Real.sqrt 2 ^ 4 = Real.sqrt 2 * (Real.sqrt 2)⁻¹ * 4
rw [mul_inv_cancel (ne_of_gt (Real.sqrt_pos.2 (show (2 : ℝ) > 0 by norm_num)))]
no goals
R : Type u
⊢ 2 > 0
norm_num
no goals
R : Type u
⊢ 0 ≤ 2
norm_num