finEquivZPowers_apply — Mathlib

English

A refined statement of the previous application describing the exact functorial behavior on elements.

Русский

Уточнённое утверждение о поведении применения эквивалентности на элементы.

LaTeX

$$finEquivZPowers hx n = ⟨x^{n}, n, zpow_natCast x n⟩$$

Lean4

@[to_additive]
theorem finEquivZPowers_apply (hx : IsOfFinOrder x) {n : Fin (orderOf x)} :
    finEquivZPowers hx n = ⟨x ^ (n : ℕ), n, zpow_natCast x n⟩ :=
  rfl

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