English
If there exists an injective map f from M1 with 1, *, inv, and / into a DivisionMonoid M2 preserving these operations, then M1 is a DivisionMonoid.
Русский
Если существует инъективное отображение f: M1 → M2, сохраняющее 1, *, обратную операцию и деление, в DivisionMonoid M2, то M1 является DivisionMonoid.
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,y)\, f(x/y)=f(x)/f(y) \land (\forall x)(\forall n)\, f(x^n)=f(x)^n \land (\forall x)(\forall n)\, f(x^n)=f(x)^n\big) \Rightarrow \text{DivisionMonoid}(M_1)$$
Lean4
/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `DivisionMonoid` if it admits an injective map
that preserves `1`, `*`, `⁻¹`, and `/` to a `DivisionMonoid`. See note [reducible non-instances] -/
@[to_additive /-- A type endowed with `0`, `+`, unary `-`, and binary `-`
is a `SubtractionMonoid` if it admits an injective map that preserves `0`, `+`, unary `-`, and
binary `-` to a `SubtractionMonoid`. This version takes custom `nsmul` and `zsmul` as `[SMul ℕ M₁]`
and `[SMul ℤ M₁]` arguments. -/
]
protected abbrev divisionMonoid [DivisionMonoid 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) : DivisionMonoid M₁ :=
{ hf.divInvMonoid f one mul inv div npow zpow, hf.involutiveInv f inv with
mul_inv_rev := fun x y => hf <| by rw [inv, mul, mul_inv_rev, mul, inv, inv],
inv_eq_of_mul := fun x y h => hf <| by rw [inv, inv_eq_of_mul_eq_one_right (by rw [← mul, h, one])] }
