Source indexedtheorem · leanprover/lean4:v4.32.0

Chebyshev.lcmUpto_eq_prod

PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Chebyshev.lean:95 to 105

Mathematical statement

Exact Lean statement

theorem lcmUpto_eq_prod (n : ℕ) : lcmUpto n = ∏ p ∈ primesLE n, p ^ ((lcmUpto n).factorization p)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem lcmUpto_eq_prod (n : ℕ) : lcmUpto n = ∏ p ∈ primesLE n, p ^ ((lcmUpto n).factorization p) := by-- note: this method is deprecated and should be changed to prod_factorization_pow_eq_self when Mathlib bumps  symm; convert prod_factorization_pow_eq_self (lcmUpto_ne_zero n)  rw [Finsupp.prod_of_support_subset _ _ _ (by simp)]  simp +contextual only [support_factorization, subset_iff, mem_primeFactors, ne_eq,    Finset.lcm_eq_zero_iff, mem_Icc, id_eq, exists_eq_right, nonpos_iff_eq_zero, one_ne_zero,    _root_.zero_le, and_true, not_false_eq_true, mem_filter, mem_range, Order.lt_add_one_iff,    and_imp]  intro p pp dp  rw [← pp.dvd_factorial]  exact dp.trans <| lcmUpto_dvd_factorial n