mulOneClass — Mathlib

Lean4
/-- A type endowed with `1` and `*` is a `MulOneClass`, if it admits a surjective map that preserves
`1` and `*` from a `MulOneClass`. See note [reducible non-instances]. -/
@[to_additive /-- A type endowed with `0` and `+` is an `AddZeroClass`, if it admits a
    surjective map that preserves `0` and `+` to an `AddZeroClass`. -/
    ]
protected abbrev mulOneClass [MulOneClass M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1)
    (mul : ∀ x y, f (x * y) = f x * f y) : MulOneClass M₂ :=
  { ‹One M₂›, ‹Mul M₂› with one_mul := hf.forall.2 fun x => by rw [← one, ← mul, one_mul],
    mul_one := hf.forall.2 fun x => by rw [← one, ← mul, mul_one] }
Похожие утверждения