map_div — Mathlib

English

Group homomorphisms preserve division: f(g/h) = f(g)/f(h).

Русский

Гомоморфизмы групп сохраняют деление: f(g/h) = f(g)/f(h).

LaTeX

$$$f\\left(\\frac{g}{h}\\right) = \\frac{f(g)}{f(h)}$.$$

Lean4

/-- Group homomorphisms preserve division. -/
@[to_additive /-- Additive group homomorphisms preserve subtraction. -/
    ]
protected theorem map_div [Group α] [DivisionMonoid β] (f : α →* β) (g h : α) : f (g / h) = f g / f h :=
  map_div f g h

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