## Stream: new members

### Topic: Notation of linear_algebra.dual

#### Nicolò Cavalleri (Oct 28 2020 at 13:55):

I don't really understand this notation:

universes u v w
variables {K : Type u} {V : Type v} {ι : Type w} [decidable_eq ι]
variables [field K] [add_comm_group V] [vector_space K V]

local notation V' := dual K V


How can lean guess the field? Or is it assuming the field is always named K? In the latter case why is it a good notation?

#### Julian Berman (Oct 28 2020 at 14:06):

Won't it be because the vector space knows it

#### Adam Topaz (Oct 28 2020 at 14:06):

This is just for V itself. E.g. you couldn't use the notation W' if W is some other vectorspace.

#### Reid Barton (Oct 28 2020 at 14:06):

right, it's not only "guessing" the field, but also the vector space

#### Nicolò Cavalleri (Oct 28 2020 at 14:09):

Oh right sorry so this is just meant to be an ad hoc notation

#### Nicolò Cavalleri (Oct 28 2020 at 14:09):

I mean it is local but still reported at the top of the file this is why I thought it was meant to be not so local

#### Nicolò Cavalleri (Oct 28 2020 at 14:11):

What do you think of the notation

localized "notation V ᵛ R := module.dual R V" in linear_algebra.dual


? I need to invent a short notation to be used in vector bundles and that is more standard

#### Adam Topaz (Oct 28 2020 at 14:17):

Wouldn't writing V ᵛ R be just as tedious as writing dual R V?

#### Reid Barton (Oct 28 2020 at 14:17):

I think we try to document local notation at the top of the file so that you can understand what is going on on line 600 by looking at line 10 and not having to find line 418 where the notation is defined.

Last updated: May 10 2021 at 17:39 UTC