rpow_mul_intCast

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Real.rpow_mul_intCast

English

For x ≥ 0 and real y, integers n, x^(y n) = (x^y)^n.

Русский

Пусть x ≥ 0, y ∈ ℝ, n ∈ ℤ. Тогда x^(y n) = (x^y)^n.

LaTeX

$$$ x^{(y \cdot n)} = (x^y)^n, \quad x \ge 0,\ y \in \mathbb{R},\ n \in \mathbb{Z} $$$

Lean4

theorem rpow_mul_intCast (hx : 0 ≤ x) (y : ℝ) (n : ℤ) : x ^ (y * n) = (x ^ y) ^ n := by rw [rpow_mul hx, rpow_intCast]

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

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

Разделы

Аффилиация

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