coeIdeal_sup — Mathlib

English

The fractional ideal attached to the join of two ideals equals the sum of their corresponding fractional ideals: ↑(I ⊔ J) = (I + J).

Русский

Дрожной идеал над присоединением двух идеалов равен сумме соответствующих дробных идеалов: ↑(I ⊔ J) = I + J.

LaTeX

$$$↑(I \sqcup J) = (I + J)$$$

Lean4

@[simp, norm_cast]
theorem coeIdeal_sup (I J : Ideal R) : ↑(I ⊔ J) = (I + J : FractionalIdeal S P) :=
  coeToSubmodule_injective <| coeSubmodule_sup _ _ _

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