equiv_apply — Mathlib

English

The forward map of the DividedPowers equivalence respects dpow: for h: I map to J and hI, hJ, n, b, the dpow in the target equals the image under e of the source dpow.

Русский

Прямое отображение эквивалентности DividedPowers сохраняет dpow: dpow_n на f(b) равняется e(dpown_n на b).

LaTeX

$$$((DividedPowers.equiv h) \\ dpow\\, n\\ b) = e\\left(hI.dpow n (e^{-1} b)\\right)$$$

Lean4

theorem equiv_apply (hI : DividedPowers I) (n : ℕ) (b : B) : (equiv h hI).dpow n b = e (hI.dpow n (e.symm b)) :=
  rfl

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