minFac_prime

Mathlib.Data.Nat.Prime.Defs

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

← MathLib Explorer

English

If n ≠ 1, then minFac(n) is prime.

Русский

Если n ≠ 1, то minFac(n) — простое число.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N}, \\\\; n \\\\neq 1 \\\\Rightarrow \\\\operatorname{Prime}(\minFac(n)).$$$

Lean4

theorem minFac_prime {n : ℕ} (n1 : n ≠ 1) : Prime (minFac n) :=
  let ⟨f2, fd, a⟩ := minFac_has_prop n1
  prime_def_lt'.2 ⟨f2, fun m m2 l d => not_le_of_gt l (a m m2 (d.trans fd))⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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