unitsMulComplexConjInv_ker — Mathlib

English

The kernel of the map unitsMulComplexConjInv is exactly the realUnits; the only units mapped to torsion-trivial are those coming from K^+.

Русский

Ядро отображения unitsMulComplexConjInv совпадает с realUnits; единицы, которые отображаются в тривиальный элемент, приходят из K^+.

LaTeX

$$$$ \\ker( unitsMulComplexConjInv_K ) = \\mathrm{realUnits}(K) $$$$

Lean4

/-- The kernel of `unitsMulComplexConjInv` is the subgroup of real units.
-/
theorem unitsMulComplexConjInv_ker : (unitsMulComplexConjInv K).ker = realUnits K :=
  by
  ext
  rw [MonoidHom.mem_ker, Subtype.ext_iff, unitsMulComplexConjInv_apply, OneMemClass.coe_one, mul_inv_eq_one, eq_comm,
    unitsComplexConj_eq_self_iff]

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