mulEquivOfOrderOfEq_apply_gen

Mathlib.GroupTheory.SpecificGroups.Cyclic

URI: https://scilib.ai/kg/mathlib#mulEquivOfOrderOfEq_apply_gen

← MathLib Explorer

English

The cardinality of MulAut G for a cyclic finite group G is φ(|G|).

Русский

Число автоморфизмов циклической группы равно эйлерову функции φ(|G|).

LaTeX

$$Nat.card (MulAut G) = Nat.totient (Nat.card G)$$

Lean4

@[to_additive (attr := simp)]
theorem mulEquivOfOrderOfEq_apply_gen : mulEquivOfOrderOfEq hg hg' h g = g' :=
  monoidHomOfForallMemZpowers_apply_gen hg h.symm.dvd

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

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

Разделы

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

Аффилиация

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