cons_self

Mathlib.Tactic.Simproc.Factors

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

Lean4

theorem cons_self {n m : ℕ} (a : ℕ) {l : List ℕ} (h : IsNat (a * m) n) (H : FactorsHelper m a l) :
    FactorsHelper n a (a :: l) := fun pa => H.cons_of_le _ h le_rfl (Nat.prime_def_minFac.1 pa).2 pa

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

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

Разделы

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

Аффилиация

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