addLinearEquiv_castAdd — Mathlib

English

For i ∈ Fin m, addLinearEquiv R m n (i.castAdd n) equals (basis R m i, 0).

Русский

Для i ∈ Fin m, addLinearEquiv R m n (i.castAdd n) равно (basis R m i, 0).

LaTeX

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

Lean4

theorem addLinearEquiv_castAdd (i : Fin m) : addLinearEquiv R m n (basis R (m + n) (i.castAdd n)) = (basis R m i, 0) :=
  by rw [addLinearEquiv, Basis.equiv_apply, Equiv.refl_apply, basisProd_castAdd]

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