sqrt_eq_cfc

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

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

English

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

Русский

Для NNReal x: sqrt(a^x) = a^(x/2).

LaTeX

$$$\\sqrt{a^x} = a^{x/2}$$$

Lean4

theorem sqrt_eq_cfc {a : A} : sqrt a = cfc NNReal.sqrt a :=
  by
  unfold sqrt
  rw [cfcₙ_eq_cfc]

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

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

Разделы

Аффилиация

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