map_div — Mathlib

English

Group homomorphisms preserve division: for all a,b ∈ G, f(a/b) = f(a)/f(b).

Русский

Гомоморфизмы групп сохраняют деление: для всех a,b ∈ G выполняется f(a/b) = f(a)/f(b).

LaTeX

$$$$ \forall a,b \in G,\ f(a/b) = f(a)/f(b). $$$$

Lean4

/-- Group homomorphisms preserve division.

See note [hom simp lemma priority] -/
@[to_additive (attr := simp mid) /-- Additive group homomorphisms preserve subtraction. -/
    ]
theorem map_div [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) : ∀ a b, f (a / b) = f a / f b :=
  map_div' _ <| map_inv f

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