instIsKleinFourOfNatNat

Mathlib.GroupTheory.SpecificGroups.Dihedral

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

English

The dihedral group D_2 (order 4) is Klein four, i.e., isomorphic to Z/2Z × Z/2Z.

Русский

Диэдральная группа D_2 (порядка 4) — это Klein_four, то есть изоморфна Z/2Z × Z/2Z.

LaTeX

$$D_2 \cong \mathbb{Z}/2\mathbb{Z} \times \mathbb{Z}/2\mathbb{Z}$$

Lean4

instance : IsKleinFour (DihedralGroup 2)
    where
  card_four := DihedralGroup.nat_card
  exponent_two := DihedralGroup.exponent

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

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

Разделы

Аффилиация

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