algebraMap_mk — Mathlib

English

The algebra map from R/I to I.ResidueField on the quotient representative matches the direct map from R.

Русский

Алгебраическое отображение из R/I в I.ResidueField на представителе частного совпадает с прямым отображением из R.

LaTeX

$$$\mathrm{algebraMap}(R/I, I.\mathrm{ResidueField})\big(\mathrm{Ideal.Quotient.mk} \ I \ x\big) = \mathrm{algebraMap}(R, I.\mathrm{ResidueField})\ x.$$$

Lean4

@[simp]
theorem algebraMap_mk (x) : algebraMap (R ⧸ I) I.ResidueField (Ideal.Quotient.mk _ x) = algebraMap R I.ResidueField x :=
  rfl

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