minSqFac_le_of_dvd — Mathlib

English

If MinSqFac(n) = some d and m≥2 with m^2|n, then d ≤ m.

Русский

Если MinSqFac(n)=some d и существует m≥2 с m^2|n, то d ≤ m.

LaTeX

$$$\\forall n\\, \\forall d\\, (MinSqFac(n)=some d) \\rightarrow \\forall m, 2\\le m, m^2|n \\rightarrow d\\le m$$$

Lean4

theorem minSqFac_le_of_dvd {n d : ℕ} (h : n.minSqFac = some d) {m} (m2 : 2 ≤ m) (md : m * m ∣ n) : d ≤ m :=
  by
  have := minSqFac_has_prop n; rw [h] at this
  have fd := minFac_dvd m
  exact
    le_trans (this.2.2 _ (minFac_prime <| ne_of_gt m2) (dvd_trans (mul_dvd_mul fd fd) md))
      (minFac_le <| lt_of_lt_of_le (by decide) m2)

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