Stream: Is there code for 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 -module ?
Johan Commelin (May 02 2020 at 11:56):
Is there nothing about this in
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
Last updated: May 07 2021 at 21:10 UTC