coe_mkOfPowEq — Mathlib

English

For any k, the natural powering inside rootsOfUnity commutes with the underlying element powers in the base ring.

Русский

Умножение в корнях единства на уровне элементов коммуницирует с обычным возведением в степень в базовом кольце.

LaTeX

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

Lean4

@[simp]
theorem coe_mkOfPowEq {ζ : M} {n : ℕ} [NeZero n] (h : ζ ^ n = 1) : ((rootsOfUnity.mkOfPowEq _ h : Mˣ) : M) = ζ :=
  rfl

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