clift_mk — Mathlib

English

The lifting built from the canonical mk map using the provided maps yields the identity on the coproduct.

Русский

Лифтинг, построенный из канонического mk с помощью заданных отображений, даёт тождество на копродукте.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem clift_mk :
    clift (mk : FreeMonoid (M ⊕ N) →* M ∗ N) (map_one inl) (map_one inr) (map_mul inl) (map_mul inr) = .id _ :=
  hom_ext rfl rfl

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