divisors_filter_squarefree_of_squarefree

English

If n is squarefree, every divisor d of n is squarefree.

Русский

Если n квадратносвободно, любой делитель d числа n квадратносвободен.

LaTeX

$$$n \\text{ squarefree} \\rightarrow \\forall d \\in n.divisors, \\ Squarefree(d)$$$

Lean4

theorem divisors_filter_squarefree_of_squarefree {n : ℕ} (hn : Squarefree n) :
    {d ∈ n.divisors | Squarefree d} = n.divisors :=
  Finset.ext fun d =>
    ⟨@Finset.filter_subset _ _ _ _ d, fun hd =>
      Finset.mem_filter.mpr ⟨hd, hn.squarefree_of_dvd (Nat.dvd_of_mem_divisors hd)⟩⟩

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