sum_repr_mul_repr — Mathlib

English

The inverse equivalence maps b' i back to g(b' i).

Русский

Обратная эквивалентность отображает b' i в g(b' i).

LaTeX

$$$(\\mathrm{b.equiv'}\\, b' f g hf hg hgf hfg)^{\\-1} (b' i) = g(b' i).$$$

Lean4

theorem sum_repr_mul_repr {ι'} [Fintype ι'] (b' : Basis ι' R M) (x : M) (i : ι) :
    (∑ j : ι', b.repr (b' j) i * b'.repr x j) = b.repr x i :=
  by
  conv_rhs => rw [← b'.sum_repr x]
  simp_rw [map_sum, map_smul, Finset.sum_apply']
  refine Finset.sum_congr rfl fun j _ => ?_
  rw [Finsupp.smul_apply, smul_eq_mul, mul_comm]

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