ofReal_pow

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.ofReal_pow

English

For all z,w ∈ ℝ, (RCLike.ofReal z) = (RCLike.ofReal w) iff z = w.

Русский

Для всех z,w ∈ ℝ, RCLike.ofReal z = RCLike.ofReal w тогда и только тогда, когда z = w.

LaTeX

$$$\forall z,w \in \mathbb{R},\ (\mathrm{RCLike}.ofReal\ z) = (\mathrm{RCLike}.ofReal\ w) \iff z = w$$$

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_pow (r : ℝ) (n : ℕ) : ((r ^ n : ℝ) : K) = (r : K) ^ n :=
  map_pow (algebraMap ℝ K) r n

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

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

Разделы

Аффилиация

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