instAlgebraQuotientIdealResidueField

English

The quotient ring R/I carries a natural algebra structure over I.ResidueField.

Русский

К этой фактор-кольцу R/I естественно относится структура алгебры над I.ResidueField.

LaTeX

$$$\text{Quotient algebra } (R/I) \text{ over } I.\mathrm{ResidueField}.$$$

Lean4

noncomputable instance : Algebra (R ⧸ I) I.ResidueField :=
  (Ideal.Quotient.liftₐ I (Algebra.ofId _ _) fun _ ↦ Ideal.algebraMap_residueField_eq_zero.mpr).toRingHom.toAlgebra

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