basisProd_natAdd — Mathlib

English

The image of the element i.natAdd m under basisProd is (0, basis R n i).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem basisProd_natAdd (m n : ℕ) (i : Fin n) : basisProd R m n (i.natAdd m) = (0, basis R n i) := by
  rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_natAdd, Basis.prod_apply, Sum.elim_inr,
    LinearMap.coe_inr, Function.comp_apply]

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