rpow_add'

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#NNReal.rpow_add'

English

For y+z ≠ 0, and x ∈ NNReal, x^{y+z} = x^y x^z.

Русский

Для y+z ≠ 0 и x ∈ ℝ≥0: x^{y+z} = x^y x^z.

LaTeX

$$$\\displaystyle x^{(y+z)} = x^{y} \\cdot x^{z} \\qquad (y+z \\neq 0)$$$

Lean4

theorem rpow_add' (h : y + z ≠ 0) (x : ℝ≥0) : x ^ (y + z) = x ^ y * x ^ z :=
  NNReal.eq <| Real.rpow_add' x.2 h

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

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

Разделы

Аффилиация

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