lift_inl_inr — Mathlib

English

There is a canonical equality of monoid homomorphisms: lift (inl, inr) equals the identity on the coproduct.

Русский

Существует каноническое равенство гомоморфизмов: lift (inl, inr) равен тождественному отображению на копродукте.

LaTeX

$$$ \operatorname{lift}(\mathrm{inl}, \mathrm{inr}) = \mathrm{id}_{G \ast H}. $$$

Lean4

@[to_additive (attr := simp)]
theorem lift_inl_inr : lift (inl : M →* M ∗ N) inr = .id _ :=
  hom_ext rfl rfl

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