instNontrivial

Mathlib.GroupTheory.SpecificGroups.Quaternion

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

English

QuaternionGroup is nontrivial for all n.

Русский

Группа QuaternionGroup ненулевая для любых n.

LaTeX

$$$\forall n, \; \text{Nontrivial}(\text{QuaternionGroup}(n))$$$

Lean4

instance : Nontrivial (QuaternionGroup n) :=
  ⟨⟨a 0, xa 0, by simp [-a_zero]⟩⟩

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

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

Разделы

Аффилиация

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