Standard basis

Stream: Is there code for X?

[Alexander Bentkamp]

Hi, I am looking for the standard basis of the vector space n → 𝕜 w.r.t 𝕜. The best I could find so far is pi.basis (λ _, basis.singleton unit 𝕜), but that has a weird indexing type. The indexing type of the basis should ideally be n.

In my case, n is finite and 𝕜 is a field, but I guess that should not really matter.

[Adam Topaz]

docs#basis.pi maybe?

[Anne Baanen]

docs#pi.basis_fun

[Anne Baanen]

The idea of docs#pi.basis is that it constructs a basis for Π i, M i given a basis for each M i

[Anne Baanen]

We should really add more references to pi.basis_fun in various places since it's a common question

[Anne Baanen]

#14505

[Alexander Bentkamp]

Thanks!