prod_primeFactors_nu — Mathlib

English

If d divides s.prodPrimes, then the product over p ∈ primeFactors(d) of ν(p) equals ν(d).

Русский

Если d делит s.prodPrimes, то произведение ν(p) по всем p, делящим d, равно ν(d).

LaTeX

$$$d \\mid s.prodPrimes \\Rightarrow \\left( \\prod_{p \\in d.primeFactors} s.nu(p) \\right) = s.nu(d)$$$

Lean4

theorem prod_primeFactors_nu {d : ℕ} (hd : d ∣ s.prodPrimes) : ∏ p ∈ d.primeFactors, s.nu p = s.nu d := by
  rw [← s.nu_mult.map_prod_of_subset_primeFactors _ _ subset_rfl,
    Nat.prod_primeFactors_of_squarefree <| Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree]

Похожие утверждения