## Stream: general

### Topic: Notation for multilinear_map

#### Eric Wieser (Feb 09 2021 at 14:10):

Any ideas for notation for docs#multilinear_map? To make things confusing, we already have (⨂ i, M i) →ₗ[R] N for docs#linear_map over docs#pi_tensor_product, which is almost isomorphic; meanwhile, (Π i, M i) →ₗ[R] N is a linear map over a pi type, which has different properties.

I came up with Πₗ i, M i →ₗ[R] N but I think it's not a good idea. Here's a mwe for someone else to try similar ideas:

import linear_algebra.multilinear

notation Πₗ  binders ,  m:(scoped:67 f, λ R, multilinear_map R f) →ₗ[R] N := m R N

example
{ι R N : Type*} {M : ι → Type*}
[semiring R] [∀ i, add_comm_monoid (M i)] [∀ i, semimodule R (M i)]
[add_comm_monoid N] [semimodule R N] :
Πₗ i, M i →ₗ[R] N :=
begin
sorry
end


#### Yury G. Kudryashov (Feb 09 2021 at 18:18):

In case of continuous_multilinear_maps we only have notation for continuous_multilinear_map (λ i : fin n, E) F

#### Eric Wieser (Feb 09 2021 at 18:38):

What is that notation? I don't remember seeing it when I last looked at docs#continuous_multilinear_map

#### Eric Wieser (Feb 09 2021 at 18:39):

Ah, M [×n]→L[R] N

#### Frédéric Dupuis (Feb 09 2021 at 19:00):

How about something like (Π i, M i) →ₘₗ[R] N?

#### Eric Wieser (Feb 09 2021 at 22:09):

Notation can't start with ( unfortunately - so that would require some clever trickery to convert Π i, M i into λ i, M i

#### Eric Wieser (Feb 09 2021 at 22:42):

I can basically get that working with:

#### Eric Wieser (Feb 09 2021 at 22:42):

But I don't know how to eliminate the sorry in the notation

#### Eric Wieser (Feb 09 2021 at 22:43):

The typeof strategy doesn't work, because it requires me to construct a term of A to use even if one doesn't exist

#### Eric Wieser (Feb 09 2021 at 22:52):

Solved!

import linear_algebra.multilinear

inductive type_info (α : Type*)
| unit [] : type_info

abbreviation type_info.codomain {α : Type*} {β : α → Type*}
(a : type_info (Π (i : α), β i)) : α → Type* := β

notation A  →ₗₘ[ R ]  N := multilinear_map R (type_info.codomain (type_info.unit A)) N

variables {ι R M N : Type*} {Mᵢ : ι → Type*}
[decidable_eq ι]
[semiring R] [∀ i, add_comm_monoid (Mᵢ i)] [∀ i, semimodule R (Mᵢ i)]

example : (Π i, Mᵢ i) →ₗₘ[R] N :=
begin
dunfold type_info.codomain, dsimp only,
exact 0,
end

example : (ι → M) →ₗₘ[R] N :=
begin
dunfold type_info.codomain, dsimp only,
exact 0,
end


#### Eric Wieser (Feb 10 2021 at 08:49):

#6152

Last updated: Dec 20 2023 at 11:08 UTC