toMonoidHomEquiv_symm_apply — Mathlib

English

The inverse of the equivalence is given by composing with Multiplicative.ofAdd.

Русский

Обратное к эквивалентности отображает обратно через композицию с Multiplicative.ofAdd.

LaTeX

$$toMonoidHomEquiv.symm φ = { toFun := φ.toFun, map_zero_eq_one' := φ.map_one', map_add_eq_mul' := φ.map_mul' }$$

Lean4

@[simp]
theorem toMonoidHomEquiv_symm_apply (ψ : Multiplicative A →* M) (a : A) :
    toMonoidHomEquiv.symm ψ a = ψ (Multiplicative.ofAdd a) :=
  rfl

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