English
For any monoid M, the submonoid IsUnit.submonoid M carries a group structure; hence it is a group.
Русский
Для любого моноида M подмоноид IsUnit.submonoid M образует группу; следовательно, он является группой.
LaTeX
$$IsUnit.submonoid M forms a Group when M is a Monoid.$$
Lean4
/-- If all the elements of a set `s` commute, then `closure s` is a commutative monoid. -/
@[to_additive /-- If all the elements of a set `s` commute, then `closure s` forms an additive
commutative monoid. -/
]
abbrev closureCommMonoidOfComm {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : CommMonoid (closure s) :=
{ (closure s).toMonoid with
mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
have := closure_le_centralizer_centralizer s
Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }
