minSqFacAux — Mathlib

English

The auxiliary function minSqFacAux is defined recursively by cases on divisibility and size of n relative to k^2.

Русский

Вспомогательная функция minSqFacAux задана рекурсивно по делимости и отношению n к k^2.

LaTeX

$$$minSqFacAux(n,k)=\\begin{cases}None,& n

Lean4

/-- Assuming that `n` has no factors less than `k`, returns the smallest prime `p` such that
  `p^2 ∣ n`. -/
def minSqFacAux : ℕ → ℕ → Option ℕ
  | n, k =>
    if h : n < k * k then none
    else
      have : Nat.sqrt n - k < Nat.sqrt n + 2 - k := by exact Nat.minFac_lemma n k h
      if k ∣ n then
        let n' := n / k
        have : Nat.sqrt n' - k < Nat.sqrt n + 2 - k := lt_of_le_of_lt (by gcongr; apply div_le_self) this
        if k ∣ n' then some k else minSqFacAux n' (k + 2)
      else minSqFacAux n (k + 2)
termination_by n k => sqrt n + 2 - k

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