primeFactorsList_ofNat

Mathlib.Tactic.Simproc.Factors

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

Lean4

/-- A simproc for terms of the form `Nat.primeFactorsList (OfNat.ofNat n)`. -/
def primeFactorsList_ofNat : Lean.Meta.Simp.Simproc :=
  .ofQ fun u α e => do
    match u, α, e with
    | 1, ~q(List ℕ), ~q(Nat.primeFactorsList (OfNat.ofNat $n)) =>
      let hn : Q(IsNat (OfNat.ofNat $n) $n) := q(⟨rfl⟩)
      let ⟨l, p⟩ ← evalPrimeFactorsList hn
      return .done <| .mk q($l) <| some q($p)
    | _ =>
      return .continue

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

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

Разделы

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

Аффилиация

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