algebraMap_eq

Mathlib.RingTheory.Ideal.Quotient.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.Quotient.algebraMap_eq

English

Same as above: If I is an ideal of a commutative ring R, then algebraMap R (R/I) equals Quotient.mk I.

Русский

То же самое: если I — идеал R, то algebraMap R (R/I) = Quotient.mk I.

LaTeX

$$$ \operatorname{algebraMap}_R (R/I) = \operatorname{Quotient.mk} I. $$$

Lean4

@[simp]
theorem algebraMap_eq {R} [CommRing R] (I : Ideal R) : algebraMap R (R ⧸ I) = Quotient.mk I :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru