English
For a submonoid P ⊆ M, FG(P) holds if and only if FG of P viewed as an AddSubmonoid (under the additive structure) holds.
Русский
Для подмоноида P ⊆ M справедливо: P является конечнопорожденным по отношению к умножению тогда и только тогда, когда он является конечнопорожденным как AddSubmonoid под той же структурой сложения.
LaTeX
$$$ FG(P) \\iff FG\\left(P^{\\mathrm{add}}\\right)$$$
Lean4
/-- An equivalent expression of `Submonoid.FG` in terms of `Set.Finite` instead of `Finset`. -/
@[to_additive /-- An equivalent expression of `AddSubmonoid.FG` in terms of `Set.Finite` instead of
`Finset`. -/
]
theorem fg_iff (P : Submonoid M) : Submonoid.FG P ↔ ∃ S : Set M, Submonoid.closure S = P ∧ S.Finite :=
⟨fun ⟨S, hS⟩ => ⟨S, hS, Finset.finite_toSet S⟩, fun ⟨S, hS, hf⟩ => ⟨Set.Finite.toFinset hf, by simp [hS]⟩⟩
