centerCharacteristic — Mathlib

English

The center Z(G) is a characteristic subgroup of G; it is preserved by every automorphism of G.

Русский

Центр Z(G) является характеристической подпгруппой G, сохраняемой всеми автоморфизмами G.

LaTeX

$$$\forall \varphi \in \operatorname{Aut}(G),\; \varphi(Z(G)) = Z(G).$$$

Lean4

@[to_additive]
instance centerCharacteristic : (center G).Characteristic :=
  by
  refine characteristic_iff_comap_le.mpr fun ϕ g hg => ?_
  rw [mem_center_iff]
  intro h
  rw [← ϕ.injective.eq_iff, map_mul, map_mul]
  exact (hg.comm (ϕ h)).symm

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