prod_apply_inr_snd — Mathlib

English

The second coordinate of the i-th right basis vector in the product basis equals the i-th basis vector of the right factor.

Русский

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

LaTeX

$$(b.prod b')(\mathrm{Sum.inr} i).2 = b' i$$

Lean4

theorem prod_apply_inr_snd (i) : (b.prod b' (Sum.inr i)).2 = b' i :=
  b'.repr.injective <| by
    ext i
    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.snd_sumFinsuppLEquivProdFinsupp]
    apply Finsupp.single_apply_left Sum.inr_injective

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