prod_apply_inl_fst — Mathlib

English

The first coordinate of the i-th left basis vector in the product basis is the i-th basis vector of the left factor.

Русский

Первая координата i-го левого базисного вектора в произведении равна i-му базисному вектору левого факторa.

LaTeX

$$(b.prod b')(\mathrm{Sum.inl} i).1 = b i$$

Lean4

theorem prod_apply_inl_fst (i) : (b.prod b' (Sum.inl i)).1 = b i :=
  b.repr.injective <| by
    ext j
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply, LinearEquiv.prodCongr_symm,
      LinearEquiv.prodCongr_apply, b.repr.apply_symm_apply, LinearEquiv.symm_symm, repr_self,
      Finsupp.fst_sumFinsuppLEquivProdFinsupp]
    apply Finsupp.single_apply_left Sum.inl_injective

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