English
If α is a semigroup, then WithOne α carries a canonical Monoid structure adjoining a unit, with multiplication defined accordingly.
Русский
Если α - полугруппа, то WithOne α естественно получает структуру монида с добавлением единицы, умножение определяется как в α там, где обе стороны из α, и единица действует как единица.
LaTeX
$$If $\alpha$ is a semigroup, then $\mathrm{WithOne}\ \alpha$ is a Monoid.$$
Lean4
@[to_additive]
instance instMonoid [Semigroup α] : Monoid (WithOne α)
where
__ := instMulOneClass
mul_assoc
| 1, b, c => by simp
| (a : α), 1, c => by simp
| (a : α), (b : α), 1 => by simp
| (a : α), (b : α), (c : α) => by simp_rw [← coe_mul, mul_assoc]
