ppow_apply

Mathlib.NumberTheory.ArithmeticFunction

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.ppow_apply

← MathLib Explorer

English

For k > 0, (f.ppow k)(x) = f(x)^k.

Русский

Для k > 0, (f.ppow k)(x) = f(x)^k.

LaTeX

$$$$ (f.ppow k)(x) = f(x)^k \quad( k > 0 ) $$$$

Lean4

@[simp]
theorem ppow_apply {f : ArithmeticFunction R} {k x : ℕ} (kpos : 0 < k) : f.ppow k x = f x ^ k := by
  rw [ppow, dif_neg (Nat.ne_of_gt kpos), coe_mk]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru