pow_apply

Mathlib.NumberTheory.ArithmeticFunction

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

English

pow(k) n equals 0 if k=0 and n=0, else n^k.

Русский

pow(k) n равно 0, если k=0 и n=0, иначе n^k.

LaTeX

$$$\text{pow}(k,n) = \begin{cases}0 & \text{если } k=0 \land n=0 \\ n^k & \text{иначе} \end{cases}$$$

Lean4

@[simp]
theorem pow_apply {k n : ℕ} : pow k n = if k = 0 ∧ n = 0 then 0 else n ^ k := by cases k <;> simp [pow]

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

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

Разделы

Аффилиация

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