unitsMulComplexConjInv — Mathlib

English

For torsion ζ, the product u ↦ u (conj u)^{-1} yields a concrete description on torsion; in particular, for ζ torsion, this equals ζ^2.

Русский

Для torsion-единицы ζ произведение ζ · (conj ζ)^{-1} равно ζ^2.

LaTeX

$$$$ unitsMulComplexConjInv(K)(ζ)=ζ^2 \\,\, (\\text{for torsion } ζ). $$$$

Lean4

/-- The map `(𝓞 K)ˣ →* torsion K` defined by `u ↦ u * (conj u)⁻¹`.
-/
noncomputable def unitsMulComplexConjInv : (𝓞 K)ˣ →* torsion K
    where
  toFun := fun u ↦ ⟨u * (unitsComplexConj K u)⁻¹, (mem_torsion K).mpr fun _ ↦ by simp⟩
  map_one' := by simp
  map_mul' := by
    intro _ _
    rw [MulMemClass.mk_mul_mk, Subtype.mk_eq_mk]
    apply coe_injective
    simp only [map_mul, mul_inv_rev, Units.val_mul, map_units_inv]
    ring

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