equiv'_apply — Mathlib

English

For finite index types ι', the standard coordinate identity holds: ∑_j b.repr (b' j) i · b'.repr x j = b.repr x i.

Русский

Для конечного типа индексов выполняется одна и та же формула преобразования координат.

LaTeX

$$$\\sum_{j \\in ι'} b.\\mathrm{repr}(b' j) i \\cdot b'.\\mathrm{repr} x j = b.\\mathrm{repr} x i.$$$

Lean4

@[simp]
theorem equiv'_apply (f : M → M') (g : M' → M) (hf hg hgf hfg) (i : ι) :
    b.equiv' b' f g hf hg hgf hfg (b i) = f (b i) :=
  b.constr_basis R _ _

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