quaternionGroup_one_isCyclic

Mathlib.GroupTheory.SpecificGroups.Quaternion

URI: https://scilib.ai/kg/mathlib#QuaternionGroup.quaternionGroup_one_isCyclic

← MathLib Explorer

English

IsCyclic(QuaternionGroup 1).

Русский

ГруппаQuaternionGroup 1 циклична.

LaTeX

$$$\text{IsCyclic}(\text{QuaternionGroup }1)$$$

Lean4

/-- In the special case `n = 1`, `Quaternion 1` is a cyclic group (of order `4`). -/
theorem quaternionGroup_one_isCyclic : IsCyclic (QuaternionGroup 1) :=
  by
  apply isCyclic_of_orderOf_eq_card
  · rw [Nat.card_eq_fintype_card, card, mul_one]
    exact orderOf_xa 0

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

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

Разделы

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

Аффилиация

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