fg_def — Mathlib

English

Submodule.fg_def expresses FG via finite span.

Русский

Submodule.fg_def выражает FG через конечный span.

LaTeX

$$$\\text{Submodule.fg_def} : N.FG \\iff \\exists S : Set M, S.Finite \\wedge span R S = N.$$$

Lean4

theorem fg_def {N : Submodule R M} : N.FG ↔ ∃ S : Set M, S.Finite ∧ span R S = N :=
  ⟨fun ⟨t, h⟩ => ⟨_, Finset.finite_toSet t, h⟩, by
    rintro ⟨t', h, rfl⟩
    rcases Finite.exists_finset_coe h with ⟨t, rfl⟩
    exact ⟨t, rfl⟩⟩

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