not_isCyclic

Mathlib.GroupTheory.SpecificGroups.Dihedral

URI: https://scilib.ai/kg/mathlib#DihedralGroup.not_isCyclic

← MathLib Explorer

English

If n ≠ 1, then the dihedral group DihedralGroup n is not cyclic.

Русский

Если n ≠ 1, то диэдральная группа DihedralGroup n не циклична.

LaTeX

$$n \neq 1 \Rightarrow IsCyclic(DihedralGroup(n)) = \text{false}$$

Lean4

theorem not_isCyclic (h1 : n ≠ 1) : ¬IsCyclic (DihedralGroup n) := fun h =>
  by
  by_cases h2 : n = 2
  · simpa [exponent, card, h2] using h.exponent_eq_card
  · exact not_commutative h1 h2 h.commutative

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

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

Разделы

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

Аффилиация

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