map_mul₂ — Mathlib

English

For f: M →* N →* P, the map distributes over multiplication in the first argument: f(m1 m2) n = f(m1) n · f(m2) n.

Русский

Для f: M →* N →* P отображение распределяется по умножению в первом аргументе: f(m1 m2) n = f(m1) n · f(m2) n.

LaTeX

$$$f(m_1m_2)\,n = f(m_1)\,n \; f(m_2)\,n$$$

Lean4

@[to_additive]
theorem map_mul₂ {_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} (f : M →* N →* P) (m₁ m₂ : M) (n : N) :
    f (m₁ * m₂) n = f m₁ n * f m₂ n :=
  (flip f n).map_mul _ _

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