minSqFac_dvd

Mathlib.Data.Nat.Squarefree

URI: https://scilib.ai/kg/mathlib#Nat.minSqFac_dvd

English

If MinSqFac(n) = some d, then d^2 divides n.

Русский

Если MinSqFac(n) = some d, то d^2 делит n.

LaTeX

$$$\\forall n, (MinSqFac(n) = some d) \\rightarrow d^2 \\mid n$$$

Lean4

theorem minSqFac_dvd {n d : ℕ} (h : n.minSqFac = some d) : d * d ∣ n :=
  by
  have := minSqFac_has_prop n
  rw [h] at this
  exact this.2.1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru