pow_dvd_iff_dvd_ordProj — Mathlib

English

For prime p and n ≠ 0, p^k divides n if and only if p^k divides ordProj_p(n).

Русский

Для простого p и n ≠ 0: p^k делит n тогда и только тогда, когда p^k делит ordProj_p(n).

LaTeX

$$$$ p \text{ prime},\ n \neq 0 \Rightarrow p^{k} \mid n \iff p^{k} \mid \operatorname{ordProj}_{p}(n). $$$$

Lean4

theorem pow_dvd_iff_dvd_ordProj {p k n : ℕ} (pp : Prime p) (hn : n ≠ 0) : p ^ k ∣ n ↔ p ^ k ∣ ordProj[p] n := by
  rw [pow_dvd_pow_iff_le_right pp.one_lt, pp.pow_dvd_iff_le_factorization hn]

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