principalUnitGroup_symm_apply — Mathlib

English

The inverse of the principalUnitGroupEquiv maps a unit in the kernel back to the corresponding unit in A.

Русский

Обратное отображение principalUnitGroupEquiv отправляет элемент ядра обратно к соответствующему элементу в A.

LaTeX

$$$\mathrm{principalUnitGroupEquiv}^{-1}(a)\in A^{\times}$ и $(\mathrm{principalUnitGroupEquiv}^{-1}(a) : K^×) = (a : K^×)$$$

Lean4

theorem principalUnitGroup_symm_apply (a : (Units.map (IsLocalRing.residue A).toMonoidHom).ker) :
    ((A.principalUnitGroupEquiv.symm a : Kˣ) : K) = ((a : Aˣ) : A) :=
  rfl

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