ofReal_pow — Mathlib

English

Let r be a real number and n a natural number. The embedding commutes with real exponentiation: ofReal(r^n) = (ofReal(r))^n.

Русский

Пусть r — вещественное число, n — натуральное число. Отображение сохраняет возведение в степень: ofReal(r^n) = (ofReal(r))^n.

LaTeX

$$$$\\operatorname{ofReal}(r^n) = (\\operatorname{ofReal}(r))^n.$$$$

Lean4

@[simp, norm_cast]
theorem ofReal_pow (r : ℝ) (n : ℕ) : ((r ^ n : ℝ) : ℂ) = (r : ℂ) ^ n := by
  induction n <;> simp [*, ofReal_mul, pow_succ]

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