coe_zpow — Mathlib

English

Raising a scalar to an integer power and then embedding into the quaternion algebra equals embedding the scalar and then taking the quaternion power.

Русский

Возведение скаляра в целую степень и затем вложение в кватернионы равно вложению скаляра и последующему возведению кватерниона в ту же степень.

LaTeX

$$$((x^z : \mathbb{R}) : \mathbb{H}(R)) = (x : \mathbb{H}(R))^z$$$

Lean4

@[norm_cast, simp]
theorem coe_zpow (x : R) (z : ℤ) : ((x ^ z : R) : ℍ[R]) = (x : ℍ[R]) ^ z :=
  map_zpow₀ (algebraMap R ℍ[R]) x z

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