map_inv — Mathlib

English

Group homomorphisms preserve inverses: f(a^{-1}) = f(a)^{-1} for all a.

Русский

Гомоморфизмы групп сохраняют обратные: f(a^{-1}) = f(a)^{-1} для всякого a.

LaTeX

$$$f(a^{-1}) = f(a)^{-1} \\quad( a\\in \\mathrm{Group} ).$$$

Lean4

/-- Group homomorphisms preserve inverse. -/
@[to_additive /-- Additive group homomorphisms preserve negation. -/
    ]
protected theorem map_inv [Group α] [DivisionMonoid β] (f : α →* β) (a : α) : f a⁻¹ = (f a)⁻¹ :=
  map_inv f _

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