squarefree_iff_minSqFac — Mathlib

English

If n ≠ 0, Squarefree n iff ∀ p, n.factorization p ≤ 1.

Русский

Если n ≠ 0, тогда Squarefree(n) эквивалентно ∀ p, n.factorization p ≤ 1.

LaTeX

$$$n \\neq 0 \\rightarrow (Squarefree(n) \\iff \\forall p, n.factorization(p) \\le 1)$$$

Lean4

theorem squarefree_iff_minSqFac {n : ℕ} : Squarefree n ↔ n.minSqFac = none :=
  by
  have := minSqFac_has_prop n
  constructor <;> intro H
  · rcases e : n.minSqFac with - | d
    · rfl
    rw [e] at this
    cases squarefree_iff_prime_squarefree.1 H _ this.1 this.2.1
  · rwa [H] at this

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