minOrder_of_prime

Mathlib.GroupTheory.Order.Min

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

English

If p is prime, then minOrder(ZMod p) = p.

Русский

Пусть p — простое; тогда minOrder(ZMod p) = p.

LaTeX

$$$\text{minOrder}(\mathbb{Z}/p\mathbb{Z}) = p$ for prime p$$

Lean4

@[simp]
theorem minOrder_of_prime {p : ℕ} (hp : p.Prime) : minOrder (ZMod p) = p := by
  rw [ZMod.minOrder hp.ne_zero hp.ne_one, hp.minFac_eq]

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

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

Разделы

Аффилиация

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