ofConjDivSelf — Mathlib

English

If z ≠ 0 in ℂ, then conj(z)/z lies on the unit circle.

Русский

Если z ≠ 0 в ℂ, то conj(z)/z лежит на единичной окружности.

LaTeX

$$$$ \\forall z \\in \\mathbb{C}, z \\neq 0 \\Rightarrow \\frac{\\overline{z}}{z} \\in \\mathbb{S}^1. $$$$

Lean4

/-- If `z` is a nonzero complex number, then `conj z / z` belongs to the unit circle. -/
@[simps]
def ofConjDivSelf (z : ℂ) (hz : z ≠ 0) : Circle where
  val := conj z / z
  property := mem_sphere_zero_iff_norm.2 <| by rw [norm_div, RCLike.norm_conj, div_self]; exact norm_ne_zero_iff.mpr hz

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