basisProd_castAdd — Mathlib

English

The image of the element i.castAdd n under basisProd corresponds to (basis R m i, 0) in the product basis.

Русский

Образ элемента i.castAdd n под действием basisProd равен (basis R m i, 0) в произведённом базисе.

LaTeX

$$$\\text{basisProd } R\\,m\\,n\\ (i.castAdd\\ n) = (\\text{basis } R\\,m\\,i, 0).$$$

Lean4

@[simp]
theorem basisProd_castAdd (m n : ℕ) (i : Fin m) : basisProd R m n (i.castAdd n) = (basis R m i, 0) := by
  rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_castAdd, Basis.prod_apply, Sum.elim_inl,
    LinearMap.coe_inl, Function.comp_apply]

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