From 98ed2a204009eaa0ef3e634669574091dc619199 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 30 Sep 2022 13:10:16 +0000 Subject: [PATCH] move(algebra/order/ring_lemmas): Rename file (#16520) Rename `algebra.order.monoid_lemmas_zero_lt` to `algebra.order.ring_lemmas` because `algebra.order.monoid_lemmas_zero_lt` is to `algebra.order.ring` what `algebra.order.monoid_lemmas` is to `algebra.order.monoid`. --- src/algebra/order/ring.lean | 5 ++--- .../order/{monoid_lemmas_zero_lt.lean => ring_lemmas.lean} | 0 2 files changed, 2 insertions(+), 3 deletions(-) rename src/algebra/order/{monoid_lemmas_zero_lt.lean => ring_lemmas.lean} (100%) diff --git a/src/algebra/order/ring.lean b/src/algebra/order/ring.lean index b8d50b646ad02..207719e1f75cb 100644 --- a/src/algebra/order/ring.lean +++ b/src/algebra/order/ring.lean @@ -4,10 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro -/ import algebra.char_zero.defs -import algebra.order.group -import algebra.order.monoid_lemmas_zero_lt -import algebra.order.sub import algebra.hom.ring +import algebra.order.group +import algebra.order.ring_lemmas import data.set.intervals.basic /-! diff --git a/src/algebra/order/monoid_lemmas_zero_lt.lean b/src/algebra/order/ring_lemmas.lean similarity index 100% rename from src/algebra/order/monoid_lemmas_zero_lt.lean rename to src/algebra/order/ring_lemmas.lean