Source indexedtheorem · leanprover/lean4:v4.32.0

Chebyshev.primeFactors_lcmUpto

PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Chebyshev.lean:76 to 88

Mathematical statement

Exact Lean statement

theorem primeFactors_lcmUpto (n : ℕ) : primeFactors (lcmUpto n) = primesLE n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem primeFactors_lcmUpto (n : ℕ) : primeFactors (lcmUpto n) = primesLE n := by  ext p  constructor  · intro h    have := prime_of_mem_primeFactors h    rw [←support_factorization, Finsupp.mem_support_iff, factorization_lcmUpto _ this] at h    simp_all  intro h  simp only [primesLE, mem_filter, mem_range, Order.lt_add_one_iff] at h  rw [Nat.mem_primeFactors]  refine ⟨h.2, ?_, ?_⟩  · convert! dvd_lcm (b := p) ?_ <;> simp_all [h.2.one_le]  · simp [lcmUpto, Finset.lcm_eq_zero_iff]