prod_primeFactors_of_squarefree — Mathlib

English

If n is squarefree, the product of its prime factors equals n.

Русский

Если n квадратно свободно, то произведение его простых факторов равно n.

LaTeX

$$$\\\\operatorname{Squarefree}(n) \\\\Rightarrow \\\\prod_{p \\in n.\\\\ primeFactors} p = n.$$$

Lean4

theorem prod_primeFactors_of_squarefree (hn : Squarefree n) : ∏ p ∈ n.primeFactors, p = n := by
  rw [← toFinset_factors, List.prod_toFinset _ hn.nodup_primeFactorsList, List.map_id',
    Nat.prod_primeFactorsList hn.ne_zero]

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