rpow_intCast — Mathlib

English

The real numbers carry a power operation defined by the real power rpow.

Русский

В числах ℝ определена операция возведения в степень через rpow.

LaTeX

$$$$ \\text{There is a binary operation }^: \\mathbb{R} \\times \\mathbb{R} \\to \\mathbb{R} \\text{ given by } x^y = \\text{rpow}(x,y). $$$$

Lean4

@[simp, norm_cast]
theorem rpow_intCast (x : ℝ) (n : ℤ) : x ^ (n : ℝ) = x ^ n := by
  simp only [rpow_def, ← Complex.ofReal_zpow, Complex.cpow_intCast, Complex.ofReal_intCast, Complex.ofReal_re]

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