isVirtuallyNilpotent

Mathlib.GroupTheory.Nilpotent

URI: https://scilib.ai/kg/mathlib#Group.IsNilpotent.isVirtuallyNilpotent

English

If a group G is nilpotent, then it is virtually nilpotent.

Русский

Если группа G нильпотентна, то она виртуально нильпотентна.

LaTeX

$$$\forall G,[Group\ G], IsNilpotent(G)\Rightarrow IsVirtuallyNilpotent(G)$$$

Lean4

theorem isVirtuallyNilpotent (hG : IsNilpotent G) : IsVirtuallyNilpotent G :=
  ⟨⊤, by simpa, inferInstance⟩

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

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

Разделы

Аффилиация

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