How to fix this?

Stream: mathlib4

[Lewis]

Why does it say "'Vector' has already been declared" when a lean file goes like "

import Mathlib.Data.Real.Basic import Mathlib.Algebra.Module.Basic import Mathlib.Data.Matrix.Basic import Mathlib.Topology.Basic open Real -- Define a vector as a function from finite indices to real numbers def Vector (n : ℕ) := Fin n → ℝ
"

Thanks a lot!

[Ruben Van de Velde]

Please read #backticks

But simply because a type called Vector has already been declared

[Alex J. Best]

docs#Vector is defined in mathlib, so you either need to pick a new name for your concept (recommended to avoid ambiguity), you could call it piVector or something as its a vector defined by a pi-type (->). Or you could work in a namespace.
Probably the best option is not to give the type Fin n → ℝ a name at all though, or if you do to make it an abbrev rather than a def. As that way you will be able to more easily make use of results concerning Fin n → ℝ that are already in mathlib.

[Notification Bot]

A message was moved from this topic to #new members > How to fix this? by Kim Morrison.