properDivisors_ofNat

Mathlib.Tactic.Simproc.Divisors

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

Lean4

/-- The dsimproc `Nat.properDivisors_ofNat` computes the finset `Nat.properDivisors n` when
`n` is a numeral. For instance, this simplifies `Nat.properDivisors 12` to `{1, 2, 3, 4, 6}`. -/
def properDivisors_ofNat : Lean.Meta.Simp.DSimproc := fun e => do
  unless e.isAppOfArity `Nat.properDivisors 1 do
    return .continue
  let some n ← fromExpr? e.appArg! |
    return .continue
  return unsafe .done <| mkSetLiteralQ q(Finset ℕ) <| ((unsafe n.properDivisors.val.unquot).map mkNatLit)

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

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

Разделы

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

Аффилиация

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