Skip to content

Update naming.md: ne_zero guidelines #789

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Timeroot wants to merge 3 commits into
base: lean4
Choose a base branch
from
Open

Update naming.md: ne_zero guidelines #789

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1f2cb79
Update naming.md: ne_zero guidelines
Timeroot Feb 18, 2026
28f31d3
-blank line
Timeroot Feb 18, 2026
8dec05b
Update templates/contribute/naming.md
Timeroot Feb 18, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 7 additions & 2 deletions templates/contribute/naming.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,8 +69,6 @@ class NeZero : Prop := sorry

-- follows rules 1 and 5
theorem neZero_iff {R : Type _} [Zero R] {n : R} : NeZero n ↔ n ≠ 0 := sorry
-- manual align is needed due to `lowerCamelCase` with several words inside `snake_case`
#align ne_zero_iff neZero_iff
Comment thread
Timeroot marked this conversation as resolved.
```

### Spelling
Expand Down Expand Up @@ -373,6 +371,11 @@ Sometimes abbreviations or alternative descriptions are easier to work
with. For example, we use `pos`, `neg`, `nonpos`, `nonneg` rather than
`zero_lt`, `lt_zero`, `le_zero`, and `zero_le`.

For a nonzero quantity, use `ne_zero` for `_ ≠ 0` or `zero_ne` for
`0 ≠ _` respectively (although the former is generally the preferred
form for theorems), rather than `nonzero`. Use `neZero` specifically
to refer to the `NeZero` typeclass.

```lean
import Mathlib.Algebra.Order.Monoid.Lemmas
import Mathlib.Algebra.Order.Ring.Lemmas
Expand All @@ -383,6 +386,8 @@ open Nat
#check mul_nonpos_of_nonneg_of_nonpos
#check add_lt_of_lt_of_nonpos
#check add_lt_of_nonpos_of_lt
#check pos_of_ne_zero
#check FractionalIdeal.coe_inv_of_ne_zero
```

These conventions are not perfect. They cannot distinguish compound
Expand Down