coe_npowRec — Mathlib

English

The underlying function of npowRec matches the ordinary power at each point.

Русский

Функция-основание npowRec совпадает с обычной степенью на каждой точке.

LaTeX

$$$\\forall n, \\; \\big(\\mathrm{npowRec}\\, n\\ f\\big)^{\\wedge} = f^{\\wedge n}$$$

Lean4

@[simp]
theorem coe_npowRec (f : α →ᵇ R) : ∀ n, ⇑(npowRec n f) = (⇑f) ^ n
  | 0 => by rw [npowRec, pow_zero, coe_one]
  | n + 1 => by rw [npowRec, pow_succ, coe_mul, coe_npowRec f n]

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