exponent_dvd_card

Mathlib.GroupTheory.Exponent

URI: https://scilib.ai/kg/mathlib#Group.exponent_dvd_card

English

For a finite group G, the exponent of G divides the order (cardinality) of G.

Русский

Для конечной группы G экспонента делит порядок (кардиналGroup) G.

LaTeX

$$$\\\\operatorname{exponent} G \\\\mid |G|$$$

Lean4

@[to_additive]
theorem exponent_dvd_card [Fintype G] : Monoid.exponent G ∣ Fintype.card G :=
  Monoid.exponent_dvd.mpr <| fun _ => orderOf_dvd_card

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

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

Разделы

Аффилиация

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