chore(algebra/order/ring): add a few aliases (#11911)

Add aliases `one_pos`, `two_pos`, `three_pos`, and `four_pos`. We used to have (some of) these lemmas. They were removed during one of cleanups but it doesn't hurt to have aliases.
leanprover-community · Feb 8, 2022 · b1269b0 · b1269b0
1 parent 85d9f21
commit b1269b0
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/src/algebra/order/ring.lean b/src/algebra/order/ring.lean
@@ -138,6 +138,11 @@ lemma zero_lt_three : 0 < (3:α) := add_pos zero_lt_two zero_lt_one
 
 lemma zero_lt_four : 0 < (4:α) := add_pos zero_lt_two zero_lt_two
 
+alias zero_lt_one ← one_pos
+alias zero_lt_two ← two_pos
+alias zero_lt_three ← three_pos
+alias zero_lt_four ← four_pos
+
 end nontrivial
 
 lemma mul_lt_mul_of_pos_left (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b :=

diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
@@ -9,7 +9,7 @@ import data.nat.basic
 # Basic properties of lists
 -/
 
-open function nat
+open function nat (hiding one_pos)
 
 namespace list
 universes u v w x