map_div₂ — Mathlib

English

For f: M →* N →* P with M a group and N a MulOneClass, f(m1/m2) n = f(m1) n / f(m2) n when the division is defined.

Русский

Для f: M →* N →* P, где M — группа, f(m1/m2) n = f(m1) n / f(m2) n.

LaTeX

$$$f(m_1/m_2)\,n = f(m_1)\,n / f(m_2)\,n$$$

Lean4

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

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