factorial_mul_dpow_eq_pow — Mathlib

English

For a in I, the nth divided power times n! equals a^n.

Русский

Для a ∈ I верно, что n! умножает n-ую деленную степень: (n)! · dpow(n)(a) = a^n.

LaTeX

$$$(n! : A) \\cdot hI.dpow(n)\\, a = a^n$$$

Lean4

theorem factorial_mul_dpow_eq_pow {n : ℕ} (ha : a ∈ I) : (n ! : A) * hI.dpow n a = a ^ n := by
  induction n with
  | zero => rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]
  | succ n ih =>
    rw [factorial_succ, mul_comm (n + 1)]
    nth_rewrite 1 [← (n + 1).choose_one_right]
    rw [← choose_symm_add, cast_mul, mul_assoc, ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]

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