coe_unitGroupToResidueFieldUnits_apply

English

For x in the unit group of A, the image under the canonical map to the residue field equals the residue class of x modulo the maximal ideal.

Русский

Для x ∈ A.unitGroup образ через каноническое отображение к остаточному полю равен остаточному классу x по максимальной идее.

LaTeX

$$(A.unitGroupToResidueFieldUnits x : IsLocalRing.ResidueField A) = Ideal.Quotient.mk _ (A.unitGroupMulEquiv x : A)$$

Lean4

@[simp]
theorem coe_unitGroupToResidueFieldUnits_apply (x : A.unitGroup) :
    (A.unitGroupToResidueFieldUnits x : IsLocalRing.ResidueField A) = Ideal.Quotient.mk _ (A.unitGroupMulEquiv x : A) :=
  rfl

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