isCyclic_iff

Mathlib.GroupTheory.SpecificGroups.Dihedral

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

← MathLib Explorer

English

IsCyclic(DihedralGroup n) holds if and only if n = 1.

Русский

IsCyclic(DihedralGroup n) имеет место тогда и только тогда, когда n = 1.

LaTeX

$$IsCyclic(DihedralGroup(n)) \iff n = 1$$

Lean4

theorem isCyclic_iff : IsCyclic (DihedralGroup n) ↔ n = 1
    where
  mp := not_imp_not.mp not_isCyclic
  mpr h := h ▸ isCyclic_of_prime_card (p := 2) nat_card

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

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

Разделы

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

Аффилиация

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