isNat_minFac_1

Mathlib.Tactic.NormNum.Prime

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

Lean4

theorem isNat_minFac_1 : {a : ℕ} → IsNat a (nat_lit 1) → IsNat a.minFac 1
  | _, ⟨rfl⟩ => ⟨minFac_one⟩

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

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

Разделы

Аффилиация

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