symm_monoidHomCongrRightEquiv — Mathlib

English

The inverse of the right-congruence with e is the right-congruence with the inverse of e.

Русский

Обратная к правой конгруэнтности по e равна правой конгруэнтности по e⁻¹.

LaTeX

$$$(\operatorname{monoidHomCongrRightEquiv}(e)).\mathrm{symm} = \operatorname{monoidHomCongrRightEquiv}(e^{-1})$.$$

Lean4

@[to_additive (attr := simp)]
theorem symm_monoidHomCongrRightEquiv (e : N₁ ≃* N₂) :
    (monoidHomCongrRightEquiv e).symm = monoidHomCongrRightEquiv (M := M) e.symm :=
  rfl

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