sqrt_algebraMap

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

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

English

The square root equals the cfc image of NNReal.sqrt via algebra map.

Русский

Квадратный корень равен образу cfc NNReal.sqrt через алгебраическое отображение.

LaTeX

$$sqrt a = cfc NNReal.sqrt a$$

Lean4

@[simp]
theorem sqrt_algebraMap {r : ℝ≥0} : sqrt (algebraMap ℝ≥0 A r) = algebraMap ℝ≥0 A (NNReal.sqrt r) := by
  rw [sqrt_eq_cfc, cfc_algebraMap]

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

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

Разделы

Аффилиация

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