divisors_ofNat

Mathlib.Tactic.Simproc.Divisors

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

Lean4

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

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

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

Разделы

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

Аффилиация

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