map_comp_mul — Mathlib

English

For any f in a class of multiplicative homomorphisms and any g,h: ι → M, we have f ∘ (g · h) = (f ∘ g) · (f ∘ h).

Русский

Для любого f из класса умножающих гомоморфизмов и любых g,h: ι → M имеем f ∘ (g · h) = (f ∘ g) · (f ∘ h).

LaTeX

$$$ f \circ (g \cdot h) = (f \circ g) \cdot (f \circ h) $$$

Lean4

@[to_additive (attr := simp)]
theorem map_comp_mul [MulHomClass F M N] (f : F) (g h : ι → M) : f ∘ (g * h) = f ∘ g * f ∘ h := by ext; simp

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