descFactorial_eq_zero_iff_lt — Mathlib

English

descFactorial(n,k) = 0 iff n < k.

Русский

descFactorial(n,k) = 0 тогда и только тогда, когда n < k.

LaTeX

$$$$\operatorname{descFactorial}(n,k) = 0 \iff n < k$$$$

Lean4

@[simp]
theorem descFactorial_eq_zero_iff_lt {n : ℕ} : ∀ {k : ℕ}, n.descFactorial k = 0 ↔ n < k
  | 0 => by simp only [descFactorial_zero, Nat.one_ne_zero, Nat.not_lt_zero]
  | succ k =>
    by
    rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, Nat.lt_succ_iff, Nat.sub_eq_zero_iff_le,
      Nat.lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]
    exact fun h _ => h

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