Notation of linear_algebra.dual

Stream: new members

[Nicolò Cavalleri]

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]

Won't it be because the vector space knows it

[Adam Topaz]

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

[Reid Barton]

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

[Nicolò Cavalleri]

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

[Nicolò Cavalleri]

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]

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]

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

[Reid Barton]

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.