sqrt_eq_rpow — Mathlib

English

For all x ∈ ℂ, Re(x^{1/2}) = sqrt((|x| + Re x)/2).

Русский

Для любого x ∈ ℂ, Re(x^{1/2}) = sqrt((|x| + Re x)/2).

LaTeX

$$For x ∈ ℂ, Re( x^{1/2} ) = \sqrt{ ( \|x\| + Re(x) ) / 2 }. $$

Lean4

theorem sqrt_eq_rpow (x : ℝ) : √x = x ^ (1 / (2 : ℝ)) :=
  by
  obtain h | h := le_or_gt 0 x
  · rw [← mul_self_inj_of_nonneg (sqrt_nonneg _) (rpow_nonneg h _), mul_self_sqrt h, ← sq, ← rpow_natCast, ← rpow_mul h]
    simp
  · have : 1 / (2 : ℝ) * π = π / (2 : ℝ) := by ring
    rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero]

Похожие утверждения