comp_mul

Mathlib.Algebra.Order.Hom.MonoidWithZero

URI: https://scilib.ai/kg/mathlib#OrderMonoidWithZeroHom.comp_mul

English

For g,f1,f2, the composition respects multiplication: g.comp (f1 * f2) = g.comp f1 * g.comp f2.

Русский

Составление сохраняет операцию умножения: g.comp (f1 * f2) = g.comp f1 * g.comp f2.

LaTeX

$$$ g \circ (f_1 * f_2) = (g \circ f_1) * (g \circ f_2) $$$

Lean4

theorem comp_mul (g : β →*₀o γ) (f₁ f₂ : α →*₀o β) : g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ :=
  ext fun _ => map_mul g _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru