addLinearEquiv_natAdd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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