ofRingEquiv_dpow — Mathlib

English

If h: I maps to J along a ring equivalence e, then transporting a divisor power along e yields dpow on the image equal to the image of the original dpow: (ofRingEquiv h hI).dpow n (e a) = e (hI.dpow n a).

Русский

Если I переходит в J по кольцевому эквиверсу e, то перенос делённых степеней вдоль e удовлетворяет: dpow_n на e(a) равняется e применения dpow_n к a в I.

LaTeX

$$$(ofRingEquiv\\ h\\ hI).dpow\\,n\\, (e\\,a) = e\\left(hI.dpow\\,n\\, a\\right)$$$

Lean4

@[simp]
theorem ofRingEquiv_dpow (hI : DividedPowers I) {n : ℕ} {b : B} :
    (ofRingEquiv h hI).dpow n b = e (hI.dpow n (e.symm b)) :=
  rfl

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