nnrpow_sqrt

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

URI: https://scilib.ai/kg/mathlib#CFC.nnrpow_sqrt

English

For any a and any NNReal x, (sqrt a)^x = a^(x/2).

Русский

Для любого a и любого x ∈ NNReal выполняется (sqrt a)^x = a^(x/2).

LaTeX

$$$(\\sqrt a)^x = a^{\\frac{x}{2}}$$$

Lean4

@[simp]
theorem nnrpow_sqrt {a : A} {x : ℝ≥0} : (sqrt a) ^ x = a ^ (x / 2) := by
  rw [sqrt_eq_nnrpow, nnrpow_nnrpow, one_div_mul_eq_div 2 x]

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

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

Разделы

Аффилиация

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