card_units

Mathlib.FieldTheory.Finite.Basic

URI: https://scilib.ai/kg/mathlib#ZMod.card_units

English

The number of units in ZMod p is p-1, i.e., |(ZMod p)ˣ| = p-1.

Русский

Число единиц в ZMod p равно p−1, то есть |(ZMod p)ˣ| = p−1.

LaTeX

$$$|\\left(\\mathbb{Z}/p\\mathbb{Z}\\right)^{\\times}| = p-1$$$

Lean4

theorem card_units (p : ℕ) [Fact p.Prime] : Fintype.card (ZMod p)ˣ = p - 1 := by rw [Fintype.card_units, card]

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

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

Разделы

Аффилиация

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