Zulip Chat Archive

Stream: general

Topic: bilinear maps

Alexander Bentkamp (Mar 06 2019 at 21:39):

Hello everybody,

Is there a definition of bilinear maps in mathlib? More specifically, I am looking for bilinear forms over the reals.

I saw in a thread called "module refactoring" that there was a definition of bilinear maps before, but it seems to have disappeared. Maybe you know where this went, @Kenny Lau ?

I have tried to chain linear maps like this:

[add_comm_group α] [vector_space  α] (f : α [] α [] )

but then I get the error:

failed to synthesize type class instance for
α : Type u_1,
_inst_1 : add_comm_group α,
_inst_2 : vector_space  α
 add_comm_group (α [] )

Any ideas?

Kenny Lau (Mar 06 2019 at 21:46):

works on my end:

import linear_algebra.tensor_product data.real.basic

universes u v

variables {α : Type u} [add_comm_group α] [vector_space  α] (f : α [] α [] )

Alexander Bentkamp (Mar 06 2019 at 22:53):

Thank you! I hadn't imported linear_algebra.tensor_product. There must be some instantiation in there that I need. Do you know which one? I don't see it.

Kenny Lau (Mar 06 2019 at 22:56):

you can use:

#check (by apply_instance : add_comm_group (α [] ))
#check (by apply_instance : module  (α [] ))

to see that the instantiations are linear_map.add_comm_group and linear_map.module: both are in linear_algebra/basic.lean

Last updated: Aug 03 2023 at 10:10 UTC