coe_pow — Mathlib

English

For x ∈ R and n ∈ ℕ, the coercion commutes with exponentiation: (x^n : ℍ) = (x : ℍ)^n.

Русский

Для x ∈ R и n ∈ ℕ вложение сохраняет степени: (x^n : ℍ) = (x : ℍ)^n.

LaTeX

$$$\bigl(x^{n} : \mathbb{H}(R;c_1,c_2,c_3)\bigr) = \bigl(x : \mathbb{H}(R;c_1,c_2,c_3)\bigr)^{n}.$$$

Lean4

@[norm_cast, simp]
theorem coe_pow (n : ℕ) : (↑(x ^ n) : ℍ[R,c₁,c₂,c₃]) = (x : ℍ[R,c₁,c₂,c₃]) ^ n :=
  (algebraMap R ℍ[R,c₁,c₂,c₃]).map_pow x n

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