map_mul_inv — Mathlib

English

Group homomorphisms preserve division: for any 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 \cdot b^{-1}) = f(a) \cdot f(b)^{-1}. $$$$

Lean4

/-- Group homomorphisms preserve division. -/
@[to_additive /-- Additive group homomorphisms preserve subtraction. -/
    ]
theorem map_mul_inv [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (a b : G) :
    f (a * b⁻¹) = f a * (f b)⁻¹ := by rw [map_mul, map_inv]

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