Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 4150728

Browse files
YaelDilliesRuben-VandeVeldemcdoll
committed
move(algebra/order/monoid/*): Relocate zero_le_one_class (#17646)
Move `zero_le_one_class` and `linear_ordered_comm_monoid_with_zero` to `algebra.order.monoid.with_zero`. This makes `algebra.order.monoid.defs` and `algebra.order.monoid.canonical.defs` not depend on `group_with_zero` anymore. And indeed we want to develop the theory of ordered additive and multiplicative monoids before mixing both worlds. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
1 parent 642c8c0 commit 4150728

File tree

8 files changed

+66
-72
lines changed

8 files changed

+66
-72
lines changed

‎counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
55
Authors: Johan Commelin, Damiano Testa, Kevin Buzzard
66
-/
77
import algebra.order.monoid.defs
8+
import algebra.order.monoid.with_zero
89

910
/-!
1011
An example of a `linear_ordered_comm_monoid_with_zero` in which the product of two positive

‎src/algebra/order/hom/monoid.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
66
import algebra.hom.group
7-
import order.hom.basic
87
import algebra.order.group.instances
8+
import algebra.order.monoid.with_zero
9+
import order.hom.basic
910

1011
/-!
1112
# Ordered monoid and group homomorphisms

‎src/algebra/order/monoid/canonical/defs.lean‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -182,10 +182,6 @@ end canonically_ordered_monoid
182182
lemma pos_of_gt {M : Type*} [canonically_ordered_add_monoid M] {n m : M} (h : n < m) : 0 < m :=
183183
lt_of_le_of_lt (zero_le _) h
184184

185-
@[priority 100] instance canonically_ordered_add_monoid.zero_le_one_class {M : Type*}
186-
[canonically_ordered_add_monoid M] [has_one M] : zero_le_one_class M :=
187-
⟨zero_le 1⟩
188-
189185
namespace ne_zero
190186

191187
lemma pos {M} (a : M) [canonically_ordered_add_monoid M] [ne_zero a] : 0 < a :=

‎src/algebra/order/monoid/defs.lean‎

Lines changed: 1 addition & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,8 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
55
-/
6+
import algebra.order.monoid.lemmas
67
import order.bounded_order
7-
import algebra.group_with_zero.defs
8-
import algebra.order.zero_le_one
98

109
/-!
1110
# Ordered monoids
@@ -82,16 +81,6 @@ class linear_ordered_add_comm_monoid (α : Type*)
8281
class linear_ordered_comm_monoid (α : Type*)
8382
extends linear_order α, ordered_comm_monoid α.
8483

85-
/-- A linearly ordered commutative monoid with a zero element. -/
86-
class linear_ordered_comm_monoid_with_zero (α : Type*)
87-
extends linear_ordered_comm_monoid α, comm_monoid_with_zero α :=
88-
(zero_le_one : (0 : α) ≤ 1)
89-
90-
@[priority 100]
91-
instance linear_ordered_comm_monoid_with_zero.zero_le_one_class
92-
[h : linear_ordered_comm_monoid_with_zero α] : zero_le_one_class α :=
93-
{ ..h }
94-
9584
/-- A linearly ordered commutative monoid with an additively absorbing `⊤` element.
9685
Instances should include number systems with an infinite element adjoined.` -/
9786
@[protect_proj, ancestor linear_ordered_add_comm_monoid has_top]

‎src/algebra/order/monoid/with_top.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
55
-/
6-
import algebra.order.monoid.order_dual
76
import algebra.hom.group
8-
import algebra.order.monoid.canonical.defs
7+
import algebra.order.monoid.order_dual
8+
import algebra.order.monoid.with_zero
99
import data.nat.cast.defs
1010

1111
/-! # Adjoining top/bottom elements to ordered monoids. -/

‎src/algebra/order/monoid/with_zero.lean‎

Lines changed: 55 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,16 +3,70 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
55
-/
6-
import algebra.order.monoid.canonical.defs
76
import algebra.group.with_one
7+
import algebra.group_with_zero
8+
import algebra.order.monoid.canonical.defs
89

910
/-!
1011
# Adjoining a zero element to an ordered monoid.
1112
-/
1213

14+
set_option old_structure_cmd true
15+
16+
open function
17+
1318
universe u
1419
variables {α : Type u}
1520

21+
/-- Typeclass for expressing that the `0` of a type is less or equal to its `1`. -/
22+
class zero_le_one_class (α : Type*) [has_zero α] [has_one α] [has_le α] :=
23+
(zero_le_one : (0 : α) ≤ 1)
24+
25+
/-- A linearly ordered commutative monoid with a zero element. -/
26+
class linear_ordered_comm_monoid_with_zero (α : Type*)
27+
extends linear_ordered_comm_monoid α, comm_monoid_with_zero α :=
28+
(zero_le_one : (0 : α) ≤ 1)
29+
30+
@[priority 100]
31+
instance linear_ordered_comm_monoid_with_zero.to_zero_le_one_class
32+
[linear_ordered_comm_monoid_with_zero α] : zero_le_one_class α :=
33+
{ ..‹linear_ordered_comm_monoid_with_zero α› }
34+
35+
@[priority 100]
36+
instance canonically_ordered_add_monoid.to_zero_le_one_class [canonically_ordered_add_monoid α]
37+
[has_one α] : zero_le_one_class α :=
38+
⟨zero_le 1⟩
39+
40+
/-- `zero_le_one` with the type argument implicit. -/
41+
@[simp] lemma zero_le_one [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] : (0 : α) ≤ 1 :=
42+
zero_le_one_class.zero_le_one
43+
44+
/-- `zero_le_one` with the type argument explicit. -/
45+
lemma zero_le_one' (α) [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] : (0 : α) ≤ 1 :=
46+
zero_le_one
47+
48+
lemma zero_le_two [preorder α] [has_one α] [add_zero_class α] [zero_le_one_class α]
49+
[covariant_class α α (+) (≤)] : (0 : α) ≤ 2 :=
50+
add_nonneg zero_le_one zero_le_one
51+
52+
lemma zero_le_three [preorder α] [has_one α] [add_zero_class α] [zero_le_one_class α]
53+
[covariant_class α α (+) (≤)] : (0 : α) ≤ 3 :=
54+
add_nonneg zero_le_two zero_le_one
55+
56+
lemma zero_le_four [preorder α] [has_one α] [add_zero_class α] [zero_le_one_class α]
57+
[covariant_class α α (+) (≤)] : (0 : α) ≤ 4 :=
58+
add_nonneg zero_le_two zero_le_two
59+
60+
lemma one_le_two [has_le α] [has_one α] [add_zero_class α] [zero_le_one_class α]
61+
[covariant_class α α (+) (≤)] : (1 : α) ≤ 2 :=
62+
calc 1 = 1 + 0 : (add_zero 1).symm
63+
... ≤ 1 + 1 : add_le_add_left zero_le_one _
64+
65+
lemma one_le_two' [has_le α] [has_one α] [add_zero_class α] [zero_le_one_class α]
66+
[covariant_class α α (swap (+)) (≤)] : (1 : α) ≤ 2 :=
67+
calc 1 = 0 + 1 : (zero_add 1).symm
68+
... ≤ 1 + 1 : add_le_add_right zero_le_one _
69+
1670
namespace with_zero
1771

1872
local attribute [semireducible] with_zero

‎src/algebra/order/ring/defs.lean‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,13 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Yaël Dillies
55
-/
6-
import order.min_max
7-
import algebra.ring.defs
8-
import algebra.order.monoid.cancel.defs
6+
97
import algebra.order.group.defs
8+
import algebra.order.monoid.cancel.defs
9+
import algebra.order.monoid.with_zero
1010
import algebra.order.ring.lemmas
11+
import algebra.ring.defs
12+
import order.min_max
1113
import tactic.nontriviality
1214

1315
/-!

‎src/algebra/order/zero_le_one.lean‎

Lines changed: 0 additions & 49 deletions
This file was deleted.

0 commit comments

Comments
 (0)