ofRingEquiv_dpow_apply — Mathlib

English

A variant of the transport lemma: for h: I maps to J with e, we still have the same dpow-transport formula for all n and a: (ofRingEquiv h hI).dpow n (e a) = e (hI.dpow n a).

Русский

Вариант леммы переноса: для h: I → J с эквивиалентностью e сохраняется формула переноса dpow для всех n и a.

LaTeX

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

Lean4

theorem ofRingEquiv_dpow_apply (hI : DividedPowers I) {n : ℕ} {a : A} :
    (ofRingEquiv h hI).dpow n (e a) = e (hI.dpow n a) := by simp

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