Name in project creation menu

Stream: lean4

[Patrick Massot]

@Marc Huisinga Explaining the project creation workflow in my class yesterday, I felt the need to explain that "Create Mathlib project"means "Create a project depending on Mathlib". Do you think you could change the wording? Maybe "Create a project using Mathlib" is better if you want to keep it short.

[Eric Wieser]

Or maybe even "Create a mathematics project"

[Jireh Loreaux]

I think "Create a mathematics project" is too vague. It should say "Mathlib" somewhere.

[Jireh Loreaux]

Aside: are we now styling it Mathlib instead of mathlib? That's a curious artifact of the Lean 3/4 transition I think.

[Patrick Massot]

I think we indeed decided to use Mathlib instead of mathlib.