MinFacHelper

Mathlib.Tactic.NormNum.Prime

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.MinFacHelper

Lean4

/-- A predicate representing partial progress in a proof of `minFac`. -/
def MinFacHelper (n k : ℕ) : Prop :=
  2 < k ∧ k % 2 = 1 ∧ k ≤ minFac n

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

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

Разделы

Аффилиация

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