notation for set of non-negative elements

Stream: maths

[Apurva Nakade]

What would be a good notation for the set of non-negative elements?
Currently I'm doing the following, but it feels like a bad hack:

import Mathlib.Algebra.Order.Nonneg.Ring

variable {𝕜 : Type*} [OrderedRing 𝕜]

set_option quotPrecheck false in
notation "𝕜≥0" => { c : 𝕜 // 0 ≤ c }

#check 𝕜≥0

Also, I'm suprised that the file#Mathlib/Mathlib/Algebra/Order/Nonneg/Ring.lean does not introduce any notation.

(Why do I need two "Mathlib"s in the file path lol?)

[Scott Morrison]

file#Algebra/Order/Nonneg/Ring

[Scott Morrison]

file#Mathlib/Algebra/Order/Nonneg/Ring

[Scott Morrison]

Linkifier fixed! My mistake.

[Scott Morrison]

(To be clear: now the initial Mathlib/ is optional.)

[Yaël Dillies]

Scott btw could the linkifier support projects depending on mathlib, at least the ones that appear on the list of projects? The motivation here is that I want to easily link to LeanCamCombi material.

[Scott Morrison]

At this moment this linkifer relies on a RewriteRule in a .htaccess file on a private server I control.

[Scott Morrison]

I'm happy to add more cases to it, but it should be considered completely unmaintained and subject to breakage at any moment. :-)

[Scott Morrison]

Currently the .htaccess file contains the lines:

RewriteRule ^mathlib4files/Mathlib/(.*)$    https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/$1.lean [R=301,L]
RewriteRule ^mathlib4files/(.*)$    https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/$1.lean [R=301,L]

I am happy to replace those with whatever you'd like, but don't want to write it myself.

[Junyan Xu]

I'm surprised too the notation isn't used in that file but it's indeed used in file#Mathlib/Algebra/Order/Ring/Lemmas