prod_apply_inr_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem prod_apply_inr_fst (i) : (b.prod b' (Sum.inr i)).1 = 0 :=
  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,
      Finsupp.fst_sumFinsuppLEquivProdFinsupp, LinearEquiv.map_zero, Finsupp.zero_apply]
    apply Finsupp.single_eq_of_ne Sum.inl_ne_inr

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