instFintypeOfNeZeroNat

Mathlib.GroupTheory.SpecificGroups.Dihedral

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

English

If n > 0, then DihedralGroup n is finite.

Русский

Если n > 0, то DihedralGroup n конечна.

LaTeX

$$n > 0 \Rightarrow Fintype(DihedralGroup(n))$$

Lean4

/-- If `0 < n`, then `DihedralGroup n` is a finite group.
-/
instance [NeZero n] : Fintype (DihedralGroup n) :=
  Fintype.ofEquiv _ fintypeHelper

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

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

Разделы

Аффилиация

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