mem_fromIdeal — Mathlib

English

Let I be an ideal of a ring R. The two-sided ideal generated by I coincides with the span of I, i.e. for every x in R, x lies in fromIdeal I if and only if x lies in span I.

Русский

Пусть I — идеал кольца R. Двусторонний идеал, порожденный I, совпадает с порождением I, то есть для каждого элемента x кольца R выполняется: x принадлежит fromIdeal I тогда и только тогда, когда x принадлежит span I.

LaTeX

$$$\forall I:\mathrm{Ideal}(R),\forall x\in R:\; x \in \mathrm{fromIdeal} I \iff x \in \mathrm{span}\,I$$$

Lean4

theorem mem_fromIdeal {I : Ideal R} {x : R} : x ∈ fromIdeal I ↔ x ∈ span I := by simp [fromIdeal]

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