English
For x in the unit group of A, the composed map sends the quotient class of x to the same unit as the direct unit map does.
Русский
Для x из единичной группы A композиция отображений отправляет класс x в эквивалентную единицу того же модуля, что и прямое отображение единиц.
LaTeX
$$((A.unitsModPrincipalUnitsEquivResidueFieldUnits).toMonoidHom (QuotientGroup.mk x)) = (A.unitGroupToResidueFieldUnits x)$$
Lean4
theorem unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply (x : A.unitGroup) :
A.unitsModPrincipalUnitsEquivResidueFieldUnits.toMonoidHom (QuotientGroup.mk x) =
A.unitGroupToResidueFieldUnits x :=
rfl
