equiv_apply' — Mathlib

English

A variant stating the same transport property for all a: (equiv h hI).dpow n (e a) = e (hI.dpow n a).

Русский

Вариант переносной формулы: dpow_n на e(a) равняется e(dpown_n(a)).

LaTeX

$$$(\\text{equiv } h hI).dpow\\,n\\, (e\\,a) = e\\left(hI.dpow\\,n\\, a\\right)$$$

Lean4

/-- Variant of `DividedPowers.equiv_apply` -/
theorem equiv_apply' (hI : DividedPowers I) {n : ℕ} {a : A} : (equiv h hI).dpow n (e a) = e (hI.dpow n a) :=
  ofRingEquiv_dpow_apply h hI

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