English
The composition of the quotient map with the principalUnitGroupEquiv is exactly the canonical unit map to the residue field units.
Русский
Сопоставление через факторгруппу и эквивалентность совпадают с каноническим отображением к единицам остаточного поля.
LaTeX
$$((A.unitsModPrincipalUnitsEquivResidueFieldUnits) : _ ⧸ _ →* _).comp (QuotientGroup.mk' (A.principalUnitGroup.subgroupOf A.unitGroup)) = A.unitGroupToResidueFieldUnits$$
Lean4
theorem unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk :
(A.unitsModPrincipalUnitsEquivResidueFieldUnits : _ ⧸ Subgroup.comap _ _ →* _).comp
(QuotientGroup.mk' (A.principalUnitGroup.subgroupOf A.unitGroup)) =
A.unitGroupToResidueFieldUnits :=
rfl
