comp_noncommCoprod — Mathlib

English

For h : P →* Q, the composition h ∘ (f.noncommCoprod g comm) equals (h ∘ f).noncommCoprod (h ∘ g) with the transported commuting data.

Русский

Для гомоморфизма h: P →* Q композиция h ∘ (f.noncommCoprod g comm) равна (h ∘ f).noncommCoprod (h ∘ g) с перенесёнными условиями коммютирования.

LaTeX

$$$ h \\circ (f.noncommCoprod g comm) = (h \\circ f).noncommCoprod (h \\circ g) (\\lambda m n, (comm m n).map h). $$$

Lean4

@[to_additive]
theorem comp_noncommCoprod {Q : Type*} [Monoid Q] (h : P →* Q) :
    h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) (fun m n ↦ (comm m n).map h) :=
  ext fun x => by simp

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