fg_iff_addSubmonoid_fg — Mathlib

English

For P : Submodule ℕ M, P.FG is equivalent to P.toAddSubmonoid.FG.

Русский

Для P : Submodule ℕ M справедливо P.FG ⇔ P.toAddSubmonoid.FG.

LaTeX

$$$P.FG \iff P.toAddSubmonoid.FG.$$$

Lean4

theorem fg_iff_addSubmonoid_fg (P : Submodule ℕ M) : P.FG ↔ P.toAddSubmonoid.FG :=
  ⟨fun ⟨S, hS⟩ => ⟨S, by simpa [← span_nat_eq_addSubmonoidClosure] using hS⟩, fun ⟨S, hS⟩ =>
    ⟨S, by simpa [← span_nat_eq_addSubmonoidClosure] using hS⟩⟩

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