monoidHomCongrLeftEquiv_trans — Mathlib

English

The isomorphism between MonoidHom M1 N and MonoidHom M2 N is induced by postcomposition with e : M1 ≃* M2.

Русский

Изоморфизм между MonoidHom M1 N и MonoidHom M2 N задаётся посткомпозицией с e : M1 ≃* M2.

LaTeX

$$$\operatorname{monoidHomCongrLeft}(e) : (M_1 \to^* N) \cong^* (M_2 \to^* N)$$$

Lean4

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

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