# Zulip Chat Archive

## 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_map`

s 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)]
[add_comm_monoid M] [semimodule R M]
[add_comm_monoid N] [semimodule R N]
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):

Last updated: Dec 20 2023 at 11:08 UTC