rpow_algebraMap — Mathlib

English

Rpow respects algebra map from NNReal to A: (algebraMap ℝ≥0 A x)^y = algebraMap ℝ≥0 A (x^y).

Русский

rpow сохраняет отображение алгебраического отображения из NNReal в A: (algebraMap x)^y = algebraMap (x^y).

LaTeX

$$$(\\text{algebraMap } ℝ≥0 A\\ x)^y = \\text{algebraMap } ℝ≥0 A (x^y)$$$

Lean4

@[simp]
theorem rpow_algebraMap {x : ℝ≥0} {y : ℝ} : (algebraMap ℝ≥0 A x) ^ y = algebraMap ℝ≥0 A (x ^ y) := by
  rw [rpow_def, cfc_algebraMap ..]

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