Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Params.valuation_eq_one_of_large_prime

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1697 to 1705

Source documentation

If a prime q ≥ n / L divides m < n, then its valuation in m is 1.

Exact Lean statement

lemma Params.valuation_eq_one_of_large_prime (P : Params) (m q : ℕ) (hm : m < P.n)
    (hm_pos : m ≠ 0) (hq : q.Prime) (hq_ge : q ≥ P.n / P.L) (hdiv : q ∣ m) :
    m.factorization q = 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Params.valuation_eq_one_of_large_prime (P : Params) (m q : ℕ) (hm : m < P.n)    (hm_pos : m ≠ 0) (hq : q.Prime) (hq_ge : q ≥ P.n / P.L) (hdiv : q ∣ m) :    m.factorization q = 1 := by  have hq_sq_gt_m : q ^ 2 > m := by    have hq_gt_sqrt_n : q > Real.sqrt P.n := P.hL'.trans_le (Nat.cast_le.mpr hq_ge)    rw [gt_iff_lt, Real.sqrt_lt] at hq_gt_sqrt_n <;> norm_cast at * <;> nlinarith  exact le_antisymm (Nat.le_of_not_lt fun h ↦ not_le.mpr hq_sq_gt_m <|    le_of_dvd (pos_of_ne_zero hm_pos) <| dvd_trans (pow_dvd_pow _ h) <|      ordProj_dvd m q) (Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp <| by aesop)