inv_def — Mathlib

English

For any z ∈ K, the inverse is given by z⁻¹ = conj(z) · (||z||^2)⁻¹, i.e., z⁻¹ = conj(z) divided by the squared norm of z (with the real scalar embedded in K).

Русский

Для любого z ∈ K обратное равно conj(z) умноженному на (||z||^2)⁻¹; то есть z⁻¹ = conj(z) / ||z||^2, где вещественный скаляр внедрён в K.

LaTeX

$$$$ z^{-1} = \overline{z} \cdot \bigl( \|z\|^2 \bigr)^{-1}. $$$$

Lean4

theorem inv_def (z : K) : z⁻¹ = conj z * ((‖z‖ ^ 2)⁻¹ : ℝ) :=
  by
  rcases eq_or_ne z 0 with (rfl | h₀)
  · simp
  · apply inv_eq_of_mul_eq_one_right
    rw [← mul_assoc, mul_conj, ofReal_inv, ofReal_pow, mul_inv_cancel₀]
    simpa

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