map_mul — Mathlib

English

Let F be a family of morphisms with a multiplicative structure. For any multiplicative homomorphism m, the image map distributes over products: (f1 * f2).map m = f1.map m * f2.map m.

Русский

Пусть существует отображение умножения под композициями. Для любого мультипликативного гомоморфизма m выполняется сохранение произведения: (f1 * f2).map m = f1.map m * f2.map m.

LaTeX

$$$\\forall m\\; (f_1 * f_2).map m = f_1.map m * f_2.map m.$$$

Lean4

@[to_additive]
protected theorem map_mul [FunLike F α β] [MulHomClass F α β] (m : F) : (f₁ * f₂).map m = f₁.map m * f₂.map m :=
  map_map₂_distrib <| map_mul m

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