English
If there exists an injective map f from a type with 1, * and inv into a group preserving these operations, then the domain is a group.
Русский
Если существует инъективное отображение f: M1 → M2, сохраняющее 1, умножение и обратимую операцию, в группу M2, то M1 является группой.
LaTeX
$$$\exists f: M_1 \to M_2\,\big(\text{Injective}(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} \land (\forall x)(\forall n)\, f(x^n)=f(x)^n \land (\forall z)\, f(z)=(f(z))\big) \Rightarrow \text{Group}(M_1)$$
Lean4
/-- A type endowed with `1`, `*` and `⁻¹` is a group, if it admits an injective map that preserves
`1`, `*` and `⁻¹` to a group. See note [reducible non-instances]. -/
@[to_additive /-- A type endowed with `0` and `+` is an additive group, if it admits an
injective map that preserves `0` and `+` to an additive group. -/
]
protected abbrev group [Group M₂] (f : M₁ → M₂) (hf : Injective 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) : Group M₁ :=
{ hf.divInvMonoid f one mul inv div npow zpow with
inv_mul_cancel := fun x => hf <| by rw [mul, inv, inv_mul_cancel, one] }
