mk_out

Mathlib.RingTheory.Ideal.Quotient.Defs

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

English

For any coset x in R/I, mk I (out(x)) returns x.

Русский

Для любого элемента coset x в R/I, mk I (out(x)) возвращает x.

LaTeX

$$$\\operatorname{mk}_I(\\operatorname{out}(x)) = x$$$

Lean4

@[simp]
theorem mk_out (x : R ⧸ I) : Ideal.Quotient.mk I (Quotient.out x) = x :=
  Quotient.out_eq x

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

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

Разделы

Аффилиация

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