normal_of_characteristic

Mathlib.Algebra.Group.Subgroup.Basic

URI: https://scilib.ai/kg/mathlib#Subgroup.normal_of_characteristic

← MathLib Explorer

English

If H is characteristic in G, then H is normal in G.

Русский

Если H характеристическая в G, то она нормальна в G.

LaTeX

$$$ H \text{ is characteristic in } G \Rightarrow H \lhd G $$$

Lean4

instance (priority := 100) normal_of_characteristic [h : H.Characteristic] : H.Normal :=
  ⟨fun a ha b => (SetLike.ext_iff.mp (h.fixed (MulAut.conj b)) a).mpr ha⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru