clift_comp_mk — Mathlib

English

The lift of the canonical mk map equals the identity on M ∗ N.

Русский

Лифтинг канонического mk-отображения даёт тождество на M ∗ N.

LaTeX

$$$ clift(\mathrm{mk}, \mathrm{map\_one\, inl}, \mathrm{map\_one\, inr}, \mathrm{map\_mul\, inl}, \mathrm{map\_mul\, inr}) = \mathrm{id}_{M\ast N}. $$$

Lean4

@[to_additive (attr := simp)]
theorem clift_comp_mk (f : FreeMonoid (M ⊕ N) →* P) (hM₁ hN₁ hM hN) : (clift f hM₁ hN₁ hM hN).comp mk = f :=
  DFunLike.ext' rfl

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