quotQuotEquivQuotSup_symm_quotQuotMk

Mathlib.RingTheory.Ideal.Quotient.Operations

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

← MathLib Explorer

English

quotQuotEquivQuotSup_symm is the inverse of quotQuotEquivQuotSup.

Русский

quotQuotEquivQuotSup_symm является обратным к quotQuotEquivQuotSup.

LaTeX

$$$(\\text{quotQuotEquivQuotSup } I J)^{-1} = \\text{quotQuotEquivQuotSup } J I$$$

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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