Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Params.initial.valuation_eq_one

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1193 to 1201

Source documentation

For √n < p prime and p ∣ m with 0 < m < n, we have ν_p(m) = 1 since p² > n ≥ m.

Exact Lean statement

lemma Params.initial.valuation_eq_one (P : Params) {p m : ℕ} (hp : p.Prime)
    (hp' : p > Real.sqrt P.n) (hm : m < P.n) (hm0 : m ≠ 0) (hpm : p ∣ m) :
    m.factorization p = 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Params.initial.valuation_eq_one (P : Params) {p m : ℕ} (hp : p.Prime)    (hp' : p > Real.sqrt P.n) (hm : m < P.n) (hm0 : m ≠ 0) (hpm : p ∣ m) :    m.factorization p = 1 := by  have : p ^ 2 ∣ m → False := fun h ↦ by    have := le_of_dvd (pos_of_ne_zero hm0) h    rw [gt_iff_lt, Real.sqrt_lt] at hp' <;> norm_cast at * <;> grind  exact le_antisymm (Nat.le_of_not_lt fun h ↦    this <| dvd_trans (pow_dvd_pow _ h) <| ordProj_dvd _ _)      (Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp <| by aesop)