Is there a defintion for a regular parametrized curve?

Stream: Is there code for X?

[Michael Novak]

Is there a definition for a regular parametrized curve (the first derivative is not zero anywhere)?

[Michael Rothgang]

I think we don't have this. (It will follow from very general abstract nonsense: a parametrised curve is regular iff it is an immersion (between the smooth manifolds $\mathbb{R}$ and your Euclidean space. The definition of immersions will hopefully be merged next week, and proving this equivalence is still some way off.)

[Michael Rothgang]

In other words: it should be fine with go ahead with making a new definition. Just expect that when merging it in mathlib, you may need to redo some proofs (or ask for help with doing so) to appeal to general nonsense instead.

[Michael Novak]

O.k, thank you very much!