map_inv — Mathlib

English

A multiplicative equivalence between groups preserves inversion: for every x in G, the image of x^{-1} equals the inverse of the image of x.

Русский

Умножающая эквивалентность между группами сохраняет обращение: для любого x в G образ x^{-1} равен обратному образу x.

LaTeX

$$$\forall x\in G:\ h(x^{-1}) = h(x)^{-1}$$$

Lean4

/-- A multiplicative equivalence of groups preserves inversion. -/
@[to_additive /-- An additive equivalence of additive groups preserves negation. -/
    ]
protected theorem map_inv [Group G] [DivisionMonoid H] (h : G ≃* H) (x : G) : h x⁻¹ = (h x)⁻¹ :=
  map_inv h x

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