asc_factorial_aux

Mathlib.Tactic.NormNum.NatFactorial

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

Lean4

theorem asc_factorial_aux (n l m a b : ℕ) (h₁ : n.ascFactorial l = a) (h₂ : (n + l).ascFactorial m = b) :
    n.ascFactorial (l + m) = a * b := by
  rw [← h₁, ← h₂]
  symm
  apply ascFactorial_mul_ascFactorial

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

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

Разделы

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

Аффилиация

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