simproc for Nat.primeFactorsList

Note that since norm_num can only produce numerals, we can't register this as a norm_num extension.

def Mathlib.Meta.Simproc.FactorsHelper (n p : ℕ) (l : List ℕ) : Prop

A proof of the partial computation of primeFactorsList. Asserts that l is a sorted list of primes multiplying to n and lower bounded by a prime p.

Equations

• Mathlib.Meta.Simproc.FactorsHelper n p l = (Nat.Prime p → List.Chain (fun (x1 x2 : ℕ) => x1 ≤ x2) p l ∧ (∀ a ∈ l, Nat.Prime a) ∧ l.prod = n)

The argument explicitness in this section is chosen to make only the numerals in the factors list appear in the proof term.

theorem Mathlib.Meta.Simproc.FactorsHelper.nil {a : ℕ} : FactorsHelper 1 a []

theorem Mathlib.Meta.Simproc.FactorsHelper.cons_of_le {n m : ℕ} (a : ℕ) {b : ℕ} {l : List ℕ} (h₁ : NormNum.IsNat (b * m) n) (h₂ : a ≤ b) (h₃ : b.minFac = b) (H : FactorsHelper m b l) : FactorsHelper n a (b :: l)

theorem Mathlib.Meta.Simproc.FactorsHelper.cons {n m a : ℕ} (b : ℕ) {l : List ℕ} (h₁ : NormNum.IsNat (b * m) n) (h₂ : a.blt b = true) (h₃ : NormNum.IsNat b.minFac b) (H : FactorsHelper m b l) : FactorsHelper n a (b :: l)

theorem Mathlib.Meta.Simproc.FactorsHelper.singleton (n : ℕ) {a : ℕ} (h₁ : a.blt n = true) (h₂ : NormNum.IsNat n.minFac n) : FactorsHelper n a [n]

theorem Mathlib.Meta.Simproc.FactorsHelper.cons_self {n m : ℕ} (a : ℕ) {l : List ℕ} (h : NormNum.IsNat (a * m) n) (H : FactorsHelper m a l) : FactorsHelper n a (a :: l)

theorem Mathlib.Meta.Simproc.FactorsHelper.singleton_self (a : ℕ) : FactorsHelper a a [a]

theorem Mathlib.Meta.Simproc.FactorsHelper.primeFactorsList_eq {n : ℕ} {l : List ℕ} (H : FactorsHelper n 2 l) : n.primeFactorsList = l

def Mathlib.Meta.Simproc.evalPrimeFactorsList {en enl : Q(ℕ)} (hn : Q(NormNum.IsNat «$en» «$enl»)) : Lean.MetaM ((l : Q(List ℕ)) × Q(«$en».primeFactorsList = «$l»))

Given a natural number n, returns (l, ⊢ Nat.primeFactorsList n = l).

Equations

• One or more equations did not get rendered due to their size.

def Nat.primeFactorsList_ofNat : Lean.Meta.Simp.Simproc

A simproc for terms of the form Nat.primeFactorsList (OfNat.ofNat n).