finEquivZPowers_symm_apply — Mathlib

English

In additive groups, the corresponding statement to powers holds for zmultiples.

Русский

В аддитивной группе соответствующее утверждение справедливо для zmultiples.

LaTeX

$$smth$$

Lean4

@[to_additive]
theorem finEquivZPowers_symm_apply (hx : IsOfFinOrder x) (n : ℕ) :
    (finEquivZPowers hx).symm ⟨x ^ n, ⟨n, by simp⟩⟩ = ⟨n % orderOf x, Nat.mod_lt _ hx.orderOf_pos⟩ := by
  rw [finEquivZPowers, Equiv.symm_trans_apply]; exact finEquivPowers_symm_apply _ n

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