monoidHomCongrRightEquiv_trans — Mathlib

English

Consecutively applying left-congruence isomorphisms corresponds to composing the underlying equivalences.

Русский

Последовательное применение левой эквивалентности конгруэнтности соответствует композиции базовых эквивалентностей.

LaTeX

$$$\operatorname{monoidHomCongrLeftEquiv}(e_1 \;\mathrm{trans}\; e_2) = (\operatorname{monoidHomCongrLeftEquiv}(e_1)).trans(\operatorname{monoidHomCongrLeftEquiv}(e_2))$$$

Lean4

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

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