coe_pow — Mathlib

English

For a root ζ in rootsOfUnity k R, its m-th power matches the m-th power of its underlying element in R.

Русский

Для корня ζ в rootsOfUnity k R m-я степень совпадает с m-й степенью базового элемента в R.

LaTeX

$$$\forall \zeta:\mathrm{rootsOfUnity}(k,R),\forall m:\mathbb{N},\; ((\zeta^m):R^{\times}) = (\zeta:\,R^{\times})^m$$$

Lean4

@[norm_cast]
theorem coe_pow [CommMonoid R] (ζ : rootsOfUnity k R) (m : ℕ) : (((ζ ^ m :) : Rˣ) : R) = ((ζ : Rˣ) : R) ^ m := by
  rw [Subgroup.coe_pow, Units.val_pow_eq_pow_val]

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