mapMulHom_comp — Mathlib

English

Composition of mapMulHom respects composition: mapMulHom (g ∘ f) = (mapMulHom g) ∘ (mapMulHom f).

Русский

Слияние mapMulHom сохраняет композицию: mapMulHom (g ∘ f) = (mapMulHom g) ∘ (mapMulHom f).

LaTeX

$$$\mathrm{mapMulHom} (g \circ f) = (\mathrm{mapMulHom} \ g) \circ (\mathrm{mapMulHom} \ f)$$$

Lean4

@[to_additive (attr := simp)]
theorem mapMulHom_comp (f : α →ₙ* β) (g : β →ₙ* γ) : mapMulHom (g.comp f) = (mapMulHom g).comp (mapMulHom f) :=
  MonoidHom.ext fun x => (mapMulHom_mapMulHom f g x).symm

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