rpow_eq_pow

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Real.rpow_eq_pow

English

For all real x,y, rpow x y equals x^y (the real power).

Русский

Для любых x,y ∈ ℝ, rpow x y равно x^y (обычную вещественную степень).

LaTeX

$$$$ \\forall x,y ∈ \\mathbb{R}, \\ rpow(x,y) = x^y. $$$$

Lean4

@[simp]
theorem rpow_eq_pow (x y : ℝ) : rpow x y = x ^ y :=
  rfl

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

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

Разделы

Аффилиация

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