How to tensor product linear functionals

Stream: new members

[Lev Stambler]

Hello, I am looking for a way to tensor product to linear functionals.

Basically, if I have Module k H and linear functions a, b : H -> k, I want to get the tensor product a \otimes b : H \otimes H -> k.

When I try to do this, I instead get H \otimes H -> k \otimes k. I am trying to see if I can replace k \otimes k with k (as they are equivalent) but have been unable to do so. I was wondering if anyone knows of any easy way to get a \otimes b : H \otimes H -> k?

[Adam Topaz]

you could just compose with docs#LinearMap.mul'

[Lev Stambler]

Thank you @Adam Topaz

Do you have any recommendations as to how to find these different statements across Mathlib or is it something that just comes with time and familiarity?

[Adam Topaz]

In this case, I found it using the following code:

import Mathlib

noncomputable section

open TensorProduct in
example (k : Type*) [Field k] : k ⊗[k] k →ₗ[k] k := exact?%

[Lev Stambler]

Okay sure. Does exact?% look for a type completion?

[Kevin Buzzard]

It looks for a declaration in mathlib whose type is the type you want (possibly after filling in holes). This might well be what you said too :-)

[Eric Wieser]

@loogle Module.Dual, TensorProduct

[loogle]

:search: TensorProduct.dualDistrib, TensorProduct.AlgebraTensorModule.dualDistrib, and 45 more

[Adomas Baliuka]

I assume exact?% is the same as by exact??

I also remember there was a way to get suggestions for how to build the current term (of type known to Lean) by typing something shorter than by exact?. But I forgot how and cannot find it anymore.

[Ruben Van de Velde]

The underscore?

[Adomas Baliuka]

Ruben Van de Velde said:

The underscore?

I don't get term suggestions when typing an underscore (like I do get when typing by exact?). Should I?

[Ruben Van de Velde]

No, but I'm not sure what else you might be referring to :)

[Yaël Dillies]

I think it's exact%?

[Ruben Van de Velde]

Yeah, but that was mentioned just above

[Yaël Dillies]

No, it was mentioned exact?% which I don't think exists

[Adam Topaz]

exact?% is the elaborator version of the tactic exact?. It’s possible another notation for it was added, but it should work.

[Lev Stambler]

Kevin Buzzard said:

It looks for a declaration in mathlib whose type is the type you want (possibly after filling in holes). This might well be what you said too :-)

Okay awesome, this is very helpful.