fg_iff_addSubgroup_fg — Mathlib

English

For P : Submodule ℤ G, P.FG is equivalent to P.toAddSubgroup.FG.

Русский

Для P : Submodule ℤ G, P.FG ⇔ P.toAddSubgroup.FG.

LaTeX

$$$P.FG \iff P.toAddSubgroup.FG.$$$

Lean4

theorem fg_iff_addSubgroup_fg {G : Type*} [AddCommGroup G] (P : Submodule ℤ G) : P.FG ↔ P.toAddSubgroup.FG :=
  ⟨fun ⟨S, hS⟩ => ⟨S, by simpa [← span_int_eq_addSubgroupClosure] using hS⟩, fun ⟨S, hS⟩ =>
    ⟨S, by simpa [← span_int_eq_addSubgroupClosure] using hS⟩⟩

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