squarefree_of_mem_divisors_prodPrimes

English

If d is a divisor of s.prodPrimes (i.e., d ∈ divisors(s.prodPrimes)), then d is squarefree.

Русский

Если d принадлежит делителям s.prodPrimes, то d квадратно свободен.

LaTeX

$$$d \\in \\operatorname{divisors}(s.prodPrimes) \\Rightarrow \\operatorname{Squarefree}(d)$$$

Lean4

theorem squarefree_of_mem_divisors_prodPrimes {d : ℕ} (hd : d ∈ divisors s.prodPrimes) : Squarefree d :=
  by
  simp only [Nat.mem_divisors] at hd
  exact Squarefree.squarefree_of_dvd hd.left s.prodPrimes_squarefree

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