instCoeQuotient

Mathlib.RingTheory.Ideal.Quotient.Defs

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

English

There is a natural coercion from R to R/I given by a ↦ a+I.

Русский

Существует естественное включение из R в R/I, задаваемое a ↦ a+I.

LaTeX

$$$\\iota: R \\to R/I,\\ iota(a) = a+I$$$

Lean4

instance : Coe R (R ⧸ I) :=
  ⟨Ideal.Quotient.mk I⟩

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

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

Разделы

Аффилиация

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