instHasEnoughRootsOfUnityHSubNatOfNat

English

There exists enough roots of unity in ZMod p of order p−1; i.e., the unit group is cyclic of order p−1.

Русский

В ZMod p существует достаточно корней единства порядка p−1; то есть группа единиц циклична и имеет порядок p−1.

LaTeX

$$$ HasEnoughRootsOfUnity\ (ZMod\ p)\ (p-1) $$$

Lean4

instance {p : ℕ} [Fact p.Prime] : HasEnoughRootsOfUnity (ZMod p) (p - 1) :=
  by
  have : NeZero (p - 1) := ⟨by have : 2 ≤ p := Nat.Prime.two_le Fact.out; grind⟩
  refine HasEnoughRootsOfUnity.of_card_le ?_
  have := Nat.card_congr (MulEquiv.subgroupCongr (ZMod.rootsOfUnity_eq_top (p := p))).toEquiv
  rw [Nat.card_eq_fintype_card] at this
  rw [this]
  simp [Fintype.card_units]

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