English
If there exists a surjective map preserving 1, multiplication, inverse, and division from M1 to a DivInvMonoid, then M1 is a DivInvMonoid.
Русский
Если существует сюръективное отображение сохраняющее 1, умножение, обратную операцию и деление, из M1 в DivInvMonoid, то M1 является DivInvMonoid.
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} \land (\forall x,y)\, f(x/y)=f(x)/f(y) \big) \Rightarrow \text{DivInvMonoid}(M_1)$$
Lean4
/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `DivInvMonoid` if it admits a surjective map
that preserves `1`, `*`, `⁻¹`, and `/` to a `DivInvMonoid`. See note [reducible non-instances]. -/
@[to_additive subNegMonoid /-- A type endowed with `0`, `+`, unary `-`, and binary `-` is a
`SubNegMonoid` if it admits a surjective map that preserves `0`, `+`, unary `-`, and binary `-` to
a `SubNegMonoid`. -/
]
protected abbrev divInvMonoid [DivInvMonoid 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) : DivInvMonoid M₂ :=
{ hf.monoid f one mul npow, ‹Div M₂›, ‹Inv M₂› with zpow := fun n x => x ^ n,
zpow_zero' := hf.forall.2 fun x => by rw [← zpow, zpow_zero, ← one],
zpow_succ' := fun n => hf.forall.2 fun x => by rw [← zpow, ← zpow, zpow_natCast, zpow_natCast, pow_succ, ← mul],
zpow_neg' := fun n => hf.forall.2 fun x => by rw [← zpow, ← zpow, zpow_negSucc, zpow_natCast, inv],
div_eq_mul_inv := hf.forall₂.2 fun x y => by rw [← inv, ← mul, ← div, div_eq_mul_inv] }
