Zulip Chat Archive

Stream: Is there code for X?

Topic: basis of free module `X -> R` with [fintype X]?


Kevin Buzzard (May 02 2020 at 11:55):

@orlando was asking me about the standard basis for finite free modules. All the std_basis machinery seems to be set up for arbitrary products (where the standard basis is not a basis). Where should he look for facts about the free RR-module RnR^n?

Johan Commelin (May 02 2020 at 11:56):

Is there nothing about this in linear_algebra/basis.lean?

Kevin Buzzard (May 02 2020 at 12:06):

There is stuff like equiv_fun_basis there Orlando -- is this enough for you?

orlando (May 02 2020 at 12:08):

hum i see also is_basis_fun ! in linear_algebra/ basis


Last updated: Dec 20 2023 at 11:08 UTC