FactorsHelper

Mathlib.Tactic.Simproc.Factors

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.Simproc.FactorsHelper

Lean4

/-- 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`. -/
def FactorsHelper (n p : ℕ) (l : List ℕ) : Prop :=
  p.Prime → (p :: l).IsChain (· ≤ ·) ∧ (∀ a ∈ l, Nat.Prime a) ∧ l.prod = n

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

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

Разделы

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

Аффилиация

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