## 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_2 : vector_space ℝ α


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: May 14 2021 at 02:15 UTC