ordProj_dvd_ordProj_iff_dvd — Mathlib

English

For nonzero a,b, (for all p, ordProj[p] a | ordProj[p] b) iff a | b.

Русский

Для ненулевых a,b выполняется: для всех p ordProj[p] a делит ordProj[p] b тогда и только тогда a делит b.

LaTeX

$$$\\forall a,b \\neq 0:\\; (\\forall p, \\ ordProj[p]\,a \\mid ordProj[p]\,b) \\iff a \\mid b$$$

Lean4

theorem ordProj_dvd_ordProj_iff_dvd (ha : a ≠ 0) (hb : b ≠ 0) : (∀ p : ℕ, ordProj[p] a ∣ ordProj[p] b) ↔ a ∣ b :=
  by
  rw [← factorization_le_iff_dvd ha hb, Finsupp.le_def]
  congr! 1 with p
  obtain _ | _ | p := p <;> simp [Nat.pow_dvd_pow_iff_le_right]

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