English
If there exists a surjective map preserving 1 and multiplication from M1 to a commutative monoid M2, then M1 is a commutative monoid.
Русский
Если существует сюръективное отображение, сохраняющее 1 и умножение, от M1 к коммутативному моноиду M2, то M1 является коммутативным моноидом.
LaTeX
$$$\exists f: M_1 \to M_2\,\big(\text{Surjective}(f) \land f(1)=1 \land (\forall x,y: M_1)\, f(xy)=f(x)f(y) \big) \Rightarrow \text{CommMonoid}(M_1)$$
Lean4
/-- A type endowed with `1` and `*` is a commutative monoid, if it admits a surjective map that
preserves `1` and `*` from a commutative monoid. See note [reducible non-instances]. -/
@[to_additive /-- A type endowed with `0` and `+` is an additive commutative monoid, if it
admits a surjective map that preserves `0` and `+` to an additive commutative monoid. -/
]
protected abbrev commMonoid [CommMonoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1)
(mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : CommMonoid M₂ :=
{ hf.commSemigroup f mul, hf.monoid f one mul npow with }
