isFractional_span_singleton — Mathlib

English

For any x, the span of the singleton {x} is a fractional ideal over S.

Русский

Для любого x, порождение одного элемента {x} образует дробный идеал над S.

LaTeX

$$$ \text{IsFractional } S (\operatorname{span} R \{x\}) $$$

Lean4

theorem isFractional_span_singleton (x : P) : IsFractional S (span R { x } : Submodule R P) :=
  let ⟨a, ha⟩ := exists_integer_multiple S x
  isFractional_span_iff.mpr ⟨a, a.2, fun _ hx' => (Set.mem_singleton_iff.mp hx').symm ▸ ha⟩

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