rpow_eq_pow

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

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

English

For all a and y, rpow a y equals a^y (the standard power).

Русский

Для всех a и y rpow a y равно a^y (стандартная степень).

LaTeX

$$$rpow\\{a\\}\\{y\\} = a^{y}$$$

Lean4

@[simp]
theorem rpow_eq_pow {a : A} {y : ℝ} : rpow a y = a ^ y :=
  rfl

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

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

Разделы

Аффилиация

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