decidablePrime_csimp

Mathlib.Data.Nat.Prime.Defs

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

English

For n ≥ 2, not Prime n is equivalent to minFac n < n.

Русский

Для n ≥ 2, не*Prime(n) эквивалентно minFac(n) < n.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N}, \\\\; 2 \\\\le n \\\\Rightarrow \\\\neg \\\\mathrm{Prime}(n) \\\\iff \\\\minFac(n) < n.$$$

Lean4

@[csimp]
theorem decidablePrime_csimp : @decidablePrime = @decidablePrime' := by subsingleton

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

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

Разделы

Аффилиация

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