ppow_succ — Mathlib

English

The successor step of ppow can also be written as f.ppow (k+1) = (f.ppow k).pmul f.

Русский

Переход к следующей степени ppow может быть записан как f.ppow (k+1) = (f.ppow k).pmul f.

LaTeX

$$$$ f.ppow (k+1) = (f.ppow k).pmul f $$$$

Lean4

theorem ppow_succ {f : ArithmeticFunction R} {k : ℕ} {kpos : 0 < k} : f.ppow (k + 1) = (f.ppow k).pmul f :=
  by
  ext x
  rw [ppow_apply (Nat.succ_pos k), _root_.pow_succ]
  induction k <;> simp

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