FG — Mathlib · SciLib

English

An ideal I of a ring R is finitely generated if there exists a finite subset S ⊆ R such that the span of S equals I.

Русский

Идеал I кольца R порождается конечным подмножеством S ⊆ R, причём порождение S равняется I.

LaTeX

$$$I.FG \iff \exists S : Finset R, \ \operatorname{span}_R(↑S) = I$$$

Lean4

/-- An ideal of `R` is finitely generated if it is the span of a finite subset of `R`.

This is defeq to `Submodule.FG`, but unfolds more nicely. -/
def FG (I : Ideal R) : Prop :=
  ∃ S : Finset R, Ideal.span ↑S = I

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