English
The equivalence between Submonoid FG and AddSubmonoid FG is preserved under the canonical additive structure.
Русский
Эквивалентность FG для подмоноида и FG для AddSubmonoid сохраняется при переходе к канонической аддитивной структуре.
LaTeX
$$$ FG(P) \\iff FG(P) \\text{ под AddSubmonoid} $ (через соответствие подмоноида) $$
Lean4
theorem fg_iff_add_fg (P : Submonoid M) : P.FG ↔ P.toAddSubmonoid.FG :=
⟨fun h =>
let ⟨S, hS, hf⟩ := (Submonoid.fg_iff _).1 h
(AddSubmonoid.fg_iff _).mpr ⟨Additive.toMul ⁻¹' S, by simp [← Submonoid.toAddSubmonoid_closure, hS], hf⟩,
fun h =>
let ⟨T, hT, hf⟩ := (AddSubmonoid.fg_iff _).1 h
(Submonoid.fg_iff _).mpr ⟨Additive.ofMul ⁻¹' T, by simp [← AddSubmonoid.toSubmonoid'_closure, hT], hf⟩⟩
