isFractional_of_fg — Mathlib

English

If the R-submodule I ⊆ P is finitely generated, then IsFractional S I holds given IsLocalization S P.

Русский

Если подмодуль I ⊆ P конечен порожден, то IsFractional S I выполняется при наличии IsLocalization S P.

LaTeX

$$$ [\\text{IsLocalization } S P] \\Rightarrow (I. FG) \\Rightarrow \\mathrm{IsFractional}\\ S I $$$

Lean4

theorem isFractional_of_fg [IsLocalization S P] {I : Submodule R P} (hI : I.FG) : IsFractional S I :=
  by
  rcases hI with ⟨I, rfl⟩
  rcases exist_integer_multiples_of_finset S I with ⟨⟨s, hs1⟩, hs⟩
  rw [isFractional_span_iff]
  exact ⟨s, hs1, hs⟩

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