Theorems · Definition · linear algebra

Pi.basisFun

(R : Type u_2) → (η : Type u_4) → [inst : Semiring R] → [Finite η] → Module.Basis η R (η → R)

The basis on η → R where the ith basis vector is Function.update 0 i 1.

Defined in

Mathlib.LinearAlgebra.StdBasis

Cited by

78 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringFinite