ker_unitGroupToResidueFieldUnits — Mathlib

English

The kernel of the canonical map from the unit group of A to the residue-field units equals the comap of the principal unit group along the unit-group inclusion.

Русский

Ядро канонического отображения от единиц A в единицы остаточного поля равно обратному образу главной группы единиц через включение единиц.

LaTeX

$$ker( A.unitGroupToResidueFieldUnits ) = A.principalUnitGroup.comap A.unitGroup.subtype$$

Lean4

theorem ker_unitGroupToResidueFieldUnits :
    A.unitGroupToResidueFieldUnits.ker = A.principalUnitGroup.comap A.unitGroup.subtype :=
  by
  ext
  simp_rw [Subgroup.mem_comap, Subgroup.coe_subtype, coe_mem_principalUnitGroup_iff, unitGroupToResidueFieldUnits,
    IsLocalRing.residue, RingHom.toMonoidHom_eq_coe, MulEquiv.toMonoidHom_eq_coe, MonoidHom.mem_ker, MonoidHom.coe_comp,
    MonoidHom.coe_coe, Function.comp_apply]

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