From b1269b0da05d1c84442a99af2a8b518d467b3cb9 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 8 Feb 2022 13:50:04 +0000 Subject: [PATCH] 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. --- src/algebra/order/ring.lean | 5 +++++ src/data/list/basic.lean | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/algebra/order/ring.lean b/src/algebra/order/ring.lean index ab39e7c302079..488416758ebd7 100644 --- 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 index 5baad9b75ebf4..6c76a3f749bfc 100644 --- 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