ordProj_dvd — Mathlib

English

For every n and p, ordProj[p] n divides n.

Русский

Для каждого n и p, ordProj[p] n делит n.

LaTeX

$$$\\operatorname{ordProj}[p]\,n \\mid n$$$

Lean4

theorem ordProj_dvd (n p : ℕ) : ordProj[p] n ∣ n :=
  by
  if hp : p.Prime then ?_ else simp [hp]
  rw [← primeFactorsList_count_eq]
  apply dvd_of_primeFactorsList_subperm (pow_ne_zero _ hp.ne_zero)
  rw [hp.primeFactorsList_pow, List.subperm_ext_iff]
  intro q hq
  simp [List.eq_of_mem_replicate hq]

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