English
The principal unit group of A is isomorphic to the kernel of the canonical map from the units of A to the units of the residue field of A.
Русский
Главная группа единиц A изоморфна ядру каноничного отображения из единиц A в единицы остаточного поля A.
LaTeX
$$$A.principalUnitGroup \cong^* \ker\Big( A.unitGroupToResidueFieldUnits \Big)$$$
Lean4
/-- The principal unit group agrees with the kernel of the canonical map from
the units of `A` to the units of the residue field of `A`. -/
def principalUnitGroupEquiv : A.principalUnitGroup ≃* (Units.map (IsLocalRing.residue A).toMonoidHom).ker
where
toFun x := ⟨A.unitGroupMulEquiv ⟨_, A.principal_units_le_units x.2⟩, A.coe_mem_principalUnitGroup_iff.1 x.2⟩
invFun x := ⟨A.unitGroupMulEquiv.symm x, by rw [A.coe_mem_principalUnitGroup_iff]; simp⟩
left_inv x := by simp
right_inv x := by simp
map_mul' _ _ := rfl
