toMonoidHomEquiv_symm_mul — Mathlib

English

The inverse of the equivalence respects multiplication to addition: toMonoidHomEquiv.symm (ψ · φ) = toMonoidHomEquiv.symm ψ + toMonoidHomEquiv.symm φ.

Русский

Обратное отображение эквивалентности переводит умножение в сложение: toMonoidHomEquiv.symm(ψ · φ) = toMonoidHomEquiv.symm ψ + toMonoidHomEquiv.symm φ.

LaTeX

$$$\mathrm{toMonoidHomEquiv}.\mathrm{symm}(\psi \cdot \phi) = \mathrm{toMonoidHomEquiv}.\mathrm{symm}(\psi) + \mathrm{toMonoidHomEquiv}.\mathrm{symm}(\phi).$$$

Lean4

@[simp]
theorem toMonoidHomEquiv_symm_mul (ψ φ : Multiplicative A →* M) :
    toMonoidHomEquiv.symm (ψ * φ) = toMonoidHomEquiv.symm ψ + toMonoidHomEquiv.symm φ :=
  rfl

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