one_rpow

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

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

English

One raised to any exponent equals itself.

Русский

Единица в любой степени равна единице.

LaTeX

$$$1^{x} = 1$$$

Lean4

@[simp]
theorem one_rpow {x : ℝ} : (1 : A) ^ x = (1 : A) := by simp [rpow_def]

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

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

Разделы

Аффилиация

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