From 1f2cb7993272eb153a3b916c92b8b57e489f2bbb Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Wed, 18 Feb 2026 12:29:56 -0500 Subject: [PATCH 1/3] Update naming.md: ne_zero guidelines also dropped old irrelevant "align" guide --- templates/contribute/naming.md | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/templates/contribute/naming.md b/templates/contribute/naming.md index 1f4a99f86e..55eb858e4e 100644 --- a/templates/contribute/naming.md +++ b/templates/contribute/naming.md @@ -69,8 +69,7 @@ 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 + ``` ### Spelling @@ -373,6 +372,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 `NeZero` instances. + ```lean import Mathlib.Algebra.Order.Monoid.Lemmas import Mathlib.Algebra.Order.Ring.Lemmas @@ -383,6 +387,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 From 28f31d377d5c09d62ba0c01cc29dc278eaac85fe Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Wed, 18 Feb 2026 12:30:39 -0500 Subject: [PATCH 2/3] -blank line --- templates/contribute/naming.md | 1 - 1 file changed, 1 deletion(-) diff --git a/templates/contribute/naming.md b/templates/contribute/naming.md index 55eb858e4e..e65e1d61c8 100644 --- a/templates/contribute/naming.md +++ b/templates/contribute/naming.md @@ -69,7 +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 - ``` ### Spelling From 8dec05b8fbe0d6af053497568e12ea126f6f44bc Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Wed, 18 Feb 2026 12:40:17 -0500 Subject: [PATCH 3/3] Update templates/contribute/naming.md Co-authored-by: Eric Wieser --- templates/contribute/naming.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/templates/contribute/naming.md b/templates/contribute/naming.md index e65e1d61c8..c739219763 100644 --- a/templates/contribute/naming.md +++ b/templates/contribute/naming.md @@ -374,7 +374,7 @@ with. For example, we use `pos`, `neg`, `nonpos`, `nonneg` rather than 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 `NeZero` instances. +to refer to the `NeZero` typeclass. ```lean import Mathlib.Algebra.Order.Monoid.Lemmas