ordProj_dvd_ordProj_of_dvd — Mathlib

English

If a divides b and b ≠ 0, then ordProj_p(a) divides ordProj_p(b) for any p.

Русский

Если a делит b и b ≠ 0, тогда ordProj_p(a) делит ordProj_p(b) для любого p.

LaTeX

$$$$ b \neq 0 \wedge a \mid b \Rightarrow \operatorname{ordProj}_{p}(a) \mid \operatorname{ordProj}_{p}(b). $$$$

Lean4

theorem ordProj_dvd_ordProj_of_dvd {a b : ℕ} (hb0 : b ≠ 0) (hab : a ∣ b) (p : ℕ) : ordProj[p] a ∣ ordProj[p] b :=
  by
  rcases em' p.Prime with (pp | pp); · simp [pp]
  rcases eq_or_ne a 0 with (rfl | ha0); · simp
  rw [pow_dvd_pow_iff_le_right pp.one_lt]
  exact (factorization_le_iff_dvd ha0 hb0).2 hab p

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