powersEquivPowers_apply — Mathlib

English

If h is an equality of orders, applying the equivalence maps x^n to y^n in a straightforward way.

Русский

Если h — равенство порядков, применение эквивалента отображает x^n в y^n напрямую.

LaTeX

$$powersEquivPowers h ⟨x^n, n, rfl⟩ = ⟨y^n, n, rfl⟩$$

Lean4

@[to_additive (attr := simp)]
theorem powersEquivPowers_apply (h : orderOf x = orderOf y) (n : ℕ) :
    powersEquivPowers h ⟨x ^ n, n, rfl⟩ = ⟨y ^ n, n, rfl⟩ :=
  by
  rw [powersEquivPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivPowers_symm_apply, ← Equiv.eq_symm_apply,
    finEquivPowers_symm_apply]
  simp [h]

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