abelianizationCongr_of — Mathlib

English

For a group isomorphism e: G ≅ H and any element x ∈ G, the induced abelianization map sends the class of x to the class of e(x).

Русский

Для изоморфизма e: G ≅ H и любого элемента x ∈ G индуцированная абелизация отображает класс x в класс e(x).

LaTeX

$$$ (e^{ab})([x]) = [e(x)], \quad x \in G, $$$

Lean4

@[simp]
theorem abelianizationCongr_of (e : G ≃* H) (x : G) :
    e.abelianizationCongr (Abelianization.of x) = Abelianization.of (e x) :=
  rfl

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