fg_iff_exists_fin_generating_family

English

For N : Submodule R M, N.FG iff exists n and a generating family s: Fin n → M with span R (range s) = N.

Русский

Для N : Submodule R M, N.FG ⇔ существует n и порождающая семья s: Fin n → M с равенством span R (range s) = N.

LaTeX

$$$N.FG \iff \exists n (s : Fin n \to M), span R (range s) = N.$$$

Lean4

theorem fg_iff_exists_fin_generating_family {N : Submodule R M} :
    N.FG ↔ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N :=
  by
  rw [fg_def]
  constructor
  · rintro ⟨S, Sfin, hS⟩
    obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding
    exact ⟨n, f, hS⟩
  · rintro ⟨n, s, hs⟩
    exact ⟨range s, finite_range s, hs⟩

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