fromIdeal — Mathlib

English

For any ideal I in R, span I is the smallest two-sided ideal containing I; i.e., if J is any two-sided ideal with I ⊆ J, then span I ⊆ J.

Русский

Для любого идеала I в кольце R span I является наименьшим двусторонним идеалом, содержащим I; то есть если J — двусторонний идеал и I ⊆ J, то span I ⊆ J.

LaTeX

$$$\\forall J \\in \\mathrm{TwoSidedIdeal}(R),\\ I \\subseteq J \\Rightarrow \\operatorname{span}(I) \\subseteq J$$$

Lean4

/-- Given an ideal `I`, `span I` is the smallest two-sided ideal containing `I`. -/
def fromIdeal : Ideal R →o TwoSidedIdeal R where
  toFun I := span I
  monotone' _ _ := span_mono

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