bilinear maps

Stream: general

[Alexander Bentkamp]

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]

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]

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]

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