zpowersEquivZPowers_apply — Mathlib

English

Under the zpowers equivalence, the image of x^n corresponds to y^n.

Русский

При эквивалентности zpowers отображение x^n переходит на y^n.

LaTeX

$$zpowersEquivZPowers_apply (h : orderOf x = orderOf y) (n : Nat) :$$

Lean4

@[to_additive (attr := simp) zmultiples_equiv_zmultiples_apply]
theorem zpowersEquivZPowers_apply (h : orderOf x = orderOf y) (n : ℕ) :
    zpowersEquivZPowers h ⟨x ^ n, n, zpow_natCast x n⟩ = ⟨y ^ n, n, zpow_natCast y n⟩ :=
  by
  rw [zpowersEquivZPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivZPowers_symm_apply, ← Equiv.eq_symm_apply,
    finEquivZPowers_symm_apply]
  simp [h]

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