sq_mul_squarefree — Mathlib

English

Let n be a natural number. Then there exist a,b ∈ ℕ such that n = b^2 · a and a is squarefree.

Русский

Пусть n — естественное число. Тогда существуют a,b ∈ ℕ такие, что n = b^2 · a и a квадратно свободно.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb N, \\\\exists a,b \\\\in \\\\mathbb N, \\\\ b^2 \\\\cdot a = n \\\\land \\\\operatorname{Squarefree}(a).$$$

Lean4

theorem sq_mul_squarefree (n : ℕ) : ∃ a b : ℕ, b ^ 2 * a = n ∧ Squarefree a :=
  by
  rcases n with - | n
  · exact ⟨1, 0, by simp, squarefree_one⟩
  · obtain ⟨a, b, -, -, h₁, h₂⟩ := sq_mul_squarefree_of_pos (succ_pos n)
    exact ⟨a, b, h₁, h₂⟩

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