surjective_unitGroupToResidueFieldUnits

English

The canonical map from the unit group of A to the unit group of the residue field is surjective.

Русский

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

LaTeX

$$Function.Surjective A.unitGroupToResidueFieldUnits$$

Lean4

theorem surjective_unitGroupToResidueFieldUnits : Function.Surjective A.unitGroupToResidueFieldUnits :=
  (IsLocalRing.surjective_units_map_of_local_ringHom _ Ideal.Quotient.mk_surjective IsLocalRing.isLocalHom_residue).comp
    (MulEquiv.surjective _)

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