English
For any n > 0 and m with n < m, the product over primes p < m of p^{v_p(n)} equals n.
Русский
Для любого n > 0 и m > n произведение по простым p < m из p^{v_p(n)} равно n.
LaTeX
$$$ \prod_{p < m,\; p \text{ prime}} p^{padicValNat p n} = n \quad (n ≠ 0,\ n < m)$$$
Lean4
theorem prod_pow_prime_padicValNat (n : Nat) (hn : n ≠ 0) (m : Nat) (pr : n < m) :
∏ p ∈ range m with p.Prime, p ^ padicValNat p n = n :=
by
nth_rw 2 [← factorization_prod_pow_eq_self hn]
rw [eq_comm]
apply Finset.prod_subset_one_on_sdiff
·
exact fun p hp =>
Finset.mem_filter.mpr
⟨Finset.mem_range.2 <| pr.trans_le' <| le_of_mem_primeFactors hp, prime_of_mem_primeFactors hp⟩
· intro p hp
obtain ⟨hp1, hp2⟩ := Finset.mem_sdiff.mp hp
rw [← factorization_def n (Finset.mem_filter.mp hp1).2]
simp [Finsupp.notMem_support_iff.mp hp2]
· intro p hp
simp [factorization_def n (prime_of_mem_primeFactors hp)]
