symm_monoidHomCongrLeftEquiv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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