instMonoidHomClass — Mathlib

English

From an EquivLike with Mul, one gets a MonoidHomClass with a special map_one proof.

Русский

Из EquivLike с Mul получается MonoidHomClass с доказательством map_one.

LaTeX

$$$\text{instMonoidHomClass}$: MonoidHomClass F M N defined using the MulEquivClass instance.$$

Lean4

@[to_additive]
instance (priority := 100) instMonoidHomClass [MulOneClass M] [MulOneClass N] [MulEquivClass F M N] :
    MonoidHomClass F M N :=
  { MulEquivClass.instMulHomClass F with
    map_one := fun e =>
      calc
        e 1 = e 1 * 1 := (mul_one _).symm
        _ = e 1 * e (EquivLike.inv e (1 : N) : M) := (congr_arg _ (EquivLike.right_inv e 1).symm)
        _ = e (EquivLike.inv e (1 : N)) := by rw [← map_mul, one_mul]
        _ = 1 := EquivLike.right_inv e 1 }

Похожие утверждения