quotLeftToQuotSup — Mathlib

English

There is a natural isomorphism between the double quotient R/(I ⊔ J) and R/(J ⊔ I).

Русский

Существует естественный изоморфизм между двойным частным R/(I ⊔ J) и R/(J ⊔ I).

LaTeX

$$$ (R \\;/ I) \\;/ J.map(\\mathrm{Quotient.mk} I) \\cong (R \\;/ J) \\;/ I.map(\\mathrm{Quotient.mk} J) $$$

Lean4

/-- The obvious ring hom `R/I → R/(I ⊔ J)` -/
def quotLeftToQuotSup : R ⧸ I →+* R ⧸ I ⊔ J :=
  Ideal.Quotient.factor le_sup_left

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