sq_mul_squarefree_of_pos' — Mathlib

English

If MinSqFac(n) = some d, then d is prime.

Русский

Если MinSqFac(n) = some d, то d простое.

LaTeX

$$$\\forall n\\, (MinSqFac(n) = some d) \\rightarrow Prime(d)$$$

Lean4

theorem sq_mul_squarefree_of_pos' {n : ℕ} (h : 0 < n) : ∃ a b : ℕ, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1) :=
  by
  obtain ⟨a₁, b₁, ha₁, hb₁, hab₁, hab₂⟩ := sq_mul_squarefree_of_pos h
  refine ⟨a₁.pred, b₁.pred, ?_, ?_⟩ <;> simpa only [add_one, succ_pred_eq_of_pos, ha₁, hb₁]

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