minSqFac_prime

Mathlib.Data.Nat.Squarefree

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

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 minSqFac_prime {n d : ℕ} (h : n.minSqFac = some d) : Prime d :=
  by
  have := minSqFac_has_prop n
  rw [h] at this
  exact this.1

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

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

Разделы

Аффилиация

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