prod_apply_inl_snd — Mathlib

English

The second coordinate of the i-th left basis vector in the product basis is zero (alternative formulation).

Русский

Вторая координата i-го левого базисного вектора в произведении равна нулю (альтернативная формулировка).

LaTeX

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

Lean4

theorem prod_apply_inl_snd (i) : (b.prod b' (Sum.inl i)).2 = 0 :=
  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,
      Finsupp.snd_sumFinsuppLEquivProdFinsupp, LinearEquiv.map_zero, Finsupp.zero_apply]
    apply Finsupp.single_eq_of_ne Sum.inr_ne_inl

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