minFacHelper_2

Mathlib.Tactic.NormNum.Prime

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.minFacHelper_2

Lean4

theorem minFacHelper_2 {n k k' : ℕ} (e : k + 2 = k') (nk : ¬Nat.Prime k) (h : MinFacHelper n k) : MinFacHelper n k' :=
  by
  refine minFacHelper_1 e h fun h2 ↦ ?_
  rw [← h2] at nk
  exact nk <| minFac_prime h.one_lt.ne'

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

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

Разделы

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

Аффилиация

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