nu_pos_of_dvd_prodPrimes — Mathlib

English

If d divides s.prodPrimes, then ν(d) > 0.

Русский

Если d делит s.prodPrimes, то ν(d) > 0.

LaTeX

$$$d \\mid s.prodPrimes \\Rightarrow 0 < s.nu(d)$$$

Lean4

theorem nu_pos_of_dvd_prodPrimes {d : ℕ} (hd : d ∣ s.prodPrimes) : 0 < s.nu d := by
  calc
    0 < ∏ p ∈ d.primeFactors, s.nu p := by
      apply prod_pos
      intro p hpd
      have hp_prime : p.Prime := prime_of_mem_primeFactors hpd
      have hp_dvd : p ∣ s.prodPrimes := (dvd_of_mem_primeFactors hpd).trans hd
      exact s.nu_pos_of_prime p hp_prime hp_dvd
    _ = s.nu d := prod_primeFactors_nu hd

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