English
In any ring S, for a natural number a, the two-term descending factorial of a, when cast to S, equals a·(a−1).
Русский
В любом кольце S для натурального a убывающий факториал длины 2 равен a·(a−1) после отображения в S.
LaTeX
$$$ (a\descFactorial 2) = a \cdot (a-1) $$$
Lean4
/-- Convenience lemma. The `a - 1` is not using truncated subtraction, as opposed to the definition
of `Nat.descFactorial` as a natural. -/
theorem cast_descFactorial_two : (a.descFactorial 2 : S) = a * (a - 1) :=
by
rw [cast_descFactorial]
cases a
· simp
·
rw [succ_sub_succ, tsub_zero, cast_succ, add_sub_cancel_right, ascPochhammer_succ_right, ascPochhammer_one,
Polynomial.X_mul, Polynomial.eval_mul_X, Polynomial.eval_add, Polynomial.eval_X, cast_one, Polynomial.eval_one]
