map_mul — Mathlib

English

If g is multiplicative, then mapping f1 and f2 by g preserves multiplication: map g (f1 * f2) = map g f1 * map g f2.

Русский

Если g сохраняет произведение, то отображение по g сохраняет умножение простых функций: map g (f1 * f2) = map g f1 * map g f2.

LaTeX

$$$\\forall g\\; (\\forall x,y, g(x\\cdot y) = g(x)\\cdot g(y))\\;\\Rightarrow\\; (f_1 \\cdot f_2).map\\ g = f_1.map\\ g \\cdot f_2.map\\ g.$$$

Lean4

@[to_additive]
theorem map_mul [Mul β] [Mul γ] {g : β → γ} (hg : ∀ x y, g (x * y) = g x * g y) (f₁ f₂ : α →ₛ β) :
    (f₁ * f₂).map g = f₁.map g * f₂.map g :=
  ext fun _ => hg _ _

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