map_mul_inv — Mathlib

English

Group homomorphisms preserve mixed products: f(g · h^{-1}) = f(g) · (f(h))^{-1}.

Русский

Гомоморфизмы сохраняют выражение вида g · h^{-1}: f(g) · (f(h))^{-1}.

LaTeX

$$$f\\bigl(g\\,h^{-1}\\bigr) = f(g)\\,(f(h))^{-1}$.$$

Lean4

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

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