exists_factorization_lt_of_lt — Mathlib

English

If a ≠ 0 and a < b, there exists a prime index p such that ν_p(a) < ν_p(b).

Русский

Если a ≠ 0 и a < b, существует индекс p, для которого ν_p(a) < ν_p(b).

LaTeX

$$$$ a \neq 0 \wedge a < b \Rightarrow \exists p: \mathbb{N},\nu_p(a) < \nu_p(b). $$$$

Lean4

theorem exists_factorization_lt_of_lt {a b : ℕ} (ha : a ≠ 0) (hab : a < b) :
    ∃ p : ℕ, a.factorization p < b.factorization p :=
  by
  have hb : b ≠ 0 := (ha.bot_lt.trans hab).ne'
  contrapose! hab
  rw [← Finsupp.le_def, factorization_le_iff_dvd hb ha] at hab
  exact le_of_dvd ha.bot_lt hab

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