to_inf_right

Mathlib.GroupTheory.PGroup

URI: https://scilib.ai/kg/mathlib#IsPGroup.to_inf_right

English

If K is a p-group, then H ∩ K is a p-group.

Русский

Если K — p-группа, то H ∩ K — p-группа.

LaTeX

$$$\IsPGroup(p,K) \rightarrow IsPGroup(p,(H \cap K : Subgroup G))$$$

Lean4

theorem to_inf_right {H K : Subgroup G} (hK : IsPGroup p K) : IsPGroup p (H ⊓ K : Subgroup G) :=
  hK.to_le inf_le_right

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

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

Разделы

Аффилиация

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