mulOneClass — Mathlib

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