# `simproc` for `Nat.primeFactorsList` #

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

source
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.IsChain (fun (x1 x2 : ℕ) => x1 ≤ x2) (p :: l) ∧ (∀ a ∈ l, Nat.Prime a) ∧ l.prod = n)

Instances For

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

source
theorem Mathlib.Meta.Simproc.FactorsHelper.nil {a : ℕ} :
FactorsHelper 1 a []
source
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)
source
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)
source
theorem Mathlib.Meta.Simproc.FactorsHelper.singleton (n : ℕ) {a : ℕ} (h₁ : a.blt n = true) (h₂ : NormNum.IsNat n.minFac n) :
FactorsHelper n a [n]
source
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)
source
theorem Mathlib.Meta.Simproc.FactorsHelper.singleton_self (a : ℕ) :
FactorsHelper a a [a]
source
theorem Mathlib.Meta.Simproc.FactorsHelper.primeFactorsList_eq {n : ℕ} {l : List ℕ} (H : FactorsHelper n 2 l) :
n.primeFactorsList = l
source
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.

Instances For

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

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

Equations

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

Instances For