quotQuotEquivQuotSup_quotQuotMk

Mathlib.RingTheory.Ideal.Quotient.Operations

URI: https://scilib.ai/kg/mathlib#DoubleQuot.quotQuotEquivQuotSup_quotQuotMk

English

quotQuotEquivQuotSup_quotQuotMk is simp

Русский

quotQuotEquivQuotSup_quotQuotMk упрощает отображение.

LaTeX

$$$\\quotQuotEquivQuotSup\\_I\\_J( quotQuotMk I J x ) = \\overline{x}^{I\\sqcup J}$$$

Lean4

@[simp]
theorem quotQuotEquivQuotSup_quotQuotMk (x : R) :
    quotQuotEquivQuotSup I J (quotQuotMk I J x) = Ideal.Quotient.mk (I ⊔ J) x :=
  rfl

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

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

Разделы

Аффилиация

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