English
If there exists a surjective map preserving 1, multiplication, and inverse from M1 to a commutative group, then M1 is a commutative group.
Русский
Если существует сюръективное отображение сохраняющее 1, умножение и обратную операцию из M1 в коммутативную группу, то 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) \land (\forall x)\, f(x^{-1})=(f(x))^{-1} \big) \Rightarrow \text{CommGroup}(M_1)$$
Lean4
/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a commutative group, if it admits a surjective
map that preserves `1`, `*`, `⁻¹`, and `/` from a commutative group. See note
[reducible non-instances]. -/
@[to_additive /-- A type endowed with `0` and `+` is an additive commutative group, if it
admits a surjective map that preserves `0` and `+` to an additive commutative group. -/
]
protected abbrev commGroup [CommGroup M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1)
(mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
(npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₂ :=
{ hf.commMonoid f one mul npow, hf.group f one mul inv div npow zpow with }
