uzpow_intCast — Mathlib

English

For u ∈ ℤˣ and z ∈ ℤ, the exponentiation respects the integer cast: u^(z) (in R) equals u^z (as an integer exponent).

Русский

Для u ∈ ℤˣ и z ∈ ℤ отображение степени согласовано с приведением к целому: u^(z) (в R) равно u^z.

LaTeX

$$$ \forall u \in \mathbb{Z}^{\times}, \forall z \in \mathbb{Z},\ u^{(z : R)} = u^{z} $$$

Lean4

@[norm_cast]
theorem uzpow_intCast (u : ℤˣ) (z : ℤ) : u ^ (z : R) = u ^ z :=
  by
  change ((z : R) • Additive.ofMul u).toMul = _
  rw [Int.cast_smul_eq_zsmul, toMul_zsmul, toMul_ofMul]

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