isNat_factorial

Mathlib.Tactic.NormNum.NatFactorial

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

Lean4

theorem isNat_factorial {n x : ℕ} (h₁ : IsNat n x) (a : ℕ) (h₂ : (1).ascFactorial x = a) : IsNat (n !) a :=
  by
  constructor
  simp only [h₁.out, cast_id, ← h₂, one_ascFactorial]

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

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

Разделы

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

Аффилиация

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