Skip to content

Commit

Permalink
move(algebra/order/ring_lemmas): Rename file (#16520)
Browse files Browse the repository at this point in the history
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`.
  • Loading branch information
YaelDillies committed Sep 30, 2022
1 parent 699c2ca commit 98ed2a2
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions src/algebra/order/ring.lean
Expand Up @@ -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

/-!
Expand Down
File renamed without changes.

0 comments on commit 98ed2a2

Please sign in to comment.