English
If d divides s.prodPrimes and d ≠ 1, then ν(d) < 1.
Русский
Если d делит s.prodPrimes и d ≠ 1, то ν(d) < 1.
LaTeX
$$$d \\mid s.prodPrimes \\land d \\neq 1 \\Rightarrow s.nu(d) < 1$$$
Lean4
theorem nu_lt_one_of_dvd_prodPrimes {d : ℕ} (hdP : d ∣ s.prodPrimes) (hd_ne_one : d ≠ 1) : s.nu d < 1 :=
by
have hd_sq : Squarefree d := Squarefree.squarefree_of_dvd hdP s.prodPrimes_squarefree
have := hd_sq.ne_zero
calc
s.nu d = ∏ p ∈ d.primeFactors, s.nu p := (prod_primeFactors_nu hdP).symm
_ < ∏ p ∈ d.primeFactors, 1 := by
apply prod_lt_prod_of_nonempty
· intro p hp
simp only [mem_primeFactors] at hp
apply s.nu_pos_of_prime p hp.1 (hp.2.1.trans hdP)
· intro p hpd; rw [mem_primeFactors_of_ne_zero hd_sq.ne_zero] at hpd
apply s.nu_lt_one_of_prime p hpd.left (hpd.2.trans hdP)
· simp only [nonempty_primeFactors, show 1 < d by cutsat]
_ = 1 := by simp
