primorial_succ

Mathlib.NumberTheory.Primorial

URI: https://scilib.ai/kg/mathlib#primorial_succ

← MathLib Explorer

English

If n is odd and n ≠ 1, then (n+1)# = n#.

Русский

Если n нечётное и n ≠ 1, то (n+1)# = n#.

LaTeX

$$(n \text{ odd} \land n \neq 1) \Rightarrow (n+1)\# = n\#$$

Lean4

theorem primorial_succ {n : ℕ} (hn1 : n ≠ 1) (hn : Odd n) : (n + 1)# = n# :=
  by
  refine prod_congr ?_ fun _ _ ↦ rfl
  rw [range_add_one, filter_insert, if_neg fun h ↦ not_even_iff_odd.2 hn _]
  exact fun h ↦ h.even_sub_one <| mt succ.inj hn1

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

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

Разделы

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

Аффилиация

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