sqrt_eq_nnrpow

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

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

English

The square root of an element a equals a raised to the power 1/2 in the NNReal sense.

Русский

Квадратный корень из элемента a равен a, возведённому в степень 1/2 в смысле NNReal.

LaTeX

$$$\\sqrt a = a^{(1/2)}$$$

Lean4

theorem sqrt_eq_nnrpow (a : A) : sqrt a = a ^ (1 / 2 : ℝ≥0) :=
  by
  simp only [sqrt]
  congr
  ext
  exact_mod_cast NNReal.sqrt_eq_rpow _

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

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

Разделы

Аффилиация

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