lean_core.data.vector

Stream: mathlib4

[Kevin Buzzard]

The porting script claims that lean_core.data.vector is high priority. First dumb question: it's not in init so I don't know where to put it in Mathlib4 (is it Mathlib.Data.Vector?). Second dumb question: is it actually high priority? If it's not (I already ported something in control which Scott told me afterwards was not actually important) then can someone give me a better algorithm for figuring out what to port next? (actually I know the answer to this -- prove that rat is an ordered field, right?)

[Mario Carneiro]

First dumb question: it's not in init so I don't know where to put it in Mathlib4 (is it Mathlib.Data.Vector?).

Yes

[Mario Carneiro]

Second dumb question: is it actually high priority?

I doubt it

[Kevin Buzzard]

OK so I'm changing my default algorithm from "look at the output of the porting script" to "look at the pdf for algebra.order.field.defs"