dvd_ordCompl_of_dvd_not_dvd — Mathlib

English

If d divides n and p does not divide d, then d divides ordCompl_p(n).

Русский

Если d делит n и p не делит d, то d делит ordCompl_p(n).

LaTeX

$$$$ d \mid n \wedge p \nmid d \Rightarrow d \mid \operatorname{ordCompl}_{p}(n). $$$$

Lean4

theorem dvd_ordCompl_of_dvd_not_dvd {p d n : ℕ} (hdn : d ∣ n) (hpd : ¬p ∣ d) : d ∣ ordCompl[p] n := by
  if hn0 : n = 0 then simp [hn0]
  else
    if hd0 : d = 0 then simp [hd0] at hpd
    else
      rw [← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne', factorization_ordCompl]
      intro q
      if hqp : q = p then simp [factorization_eq_zero_iff, hqp, hpd]
      else simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]

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