Skip to content

Commit ed38b3a

Browse files
zeramorphiczeramorphic
committed
feat: port Algebra.Order.Monoid.[TypeTags, Units] (#873)
mathlib3 SHA: f1a2caaf51ef593799107fe9a8d5e411599f3996
1 parent 4bd624b commit ed38b3a

File tree

3 files changed

+222
-0
lines changed

3 files changed

+222
-0
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,8 @@ import Mathlib.Algebra.Order.Monoid.Defs
4545
import Mathlib.Algebra.Order.Monoid.Lemmas
4646
import Mathlib.Algebra.Order.Monoid.MinMax
4747
import Mathlib.Algebra.Order.Monoid.OrderDual
48+
import Mathlib.Algebra.Order.Monoid.TypeTags
49+
import Mathlib.Algebra.Order.Monoid.Units
4850
import Mathlib.Algebra.Order.Monoid.WithZero.Basic
4951
import Mathlib.Algebra.Order.Monoid.WithZero.Defs
5052
import Mathlib.Algebra.Order.Ring

‎Mathlib/Algebra/Order/Monoid/TypeTags.lean‎

Lines changed: 163 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,163 @@
1+
/-
2+
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
5+
-/
6+
import Mathlib.Algebra.Group.TypeTags
7+
import Mathlib.Algebra.Order.Monoid.Cancel.Defs
8+
import Mathlib.Algebra.Order.Monoid.Canonical.Defs
9+
10+
/-! # Ordered monoid structures on `Multiplicative α` and `Additive α`. -/
11+
12+
13+
instance : ∀ [LE α], LE (Multiplicative α) :=
14+
fun {inst} => inst
15+
16+
instance : ∀ [LE α], LE (Additive α) :=
17+
fun {inst} => inst
18+
19+
instance : ∀ [LT α], LT (Multiplicative α) :=
20+
fun {inst} => inst
21+
22+
instance : ∀ [LT α], LT (Additive α) :=
23+
fun {inst} => inst
24+
25+
instance Multiplicative.preorder : ∀ [Preorder α], Preorder (Multiplicative α) :=
26+
fun {inst} => inst
27+
28+
instance Additive.preorder : ∀ [Preorder α], Preorder (Additive α) :=
29+
fun {inst} => inst
30+
31+
instance Multiplicative.partialOrder : ∀ [PartialOrder α], PartialOrder (Multiplicative α) :=
32+
fun {inst} => inst
33+
34+
instance Additive.partialOrder : ∀ [PartialOrder α], PartialOrder (Additive α) :=
35+
fun {inst} => inst
36+
37+
instance Multiplicative.linearOrder : ∀ [LinearOrder α], LinearOrder (Multiplicative α) :=
38+
fun {inst} => inst
39+
40+
instance Additive.linearOrder : ∀ [LinearOrder α], LinearOrder (Additive α) :=
41+
fun {inst} => inst
42+
43+
instance Multiplicative.orderBot [LE α] : ∀ [OrderBot α], OrderBot (Multiplicative α) :=
44+
fun {inst} => inst
45+
46+
instance Additive.orderBot [LE α] : ∀ [OrderBot α], OrderBot (Additive α) :=
47+
fun {inst} => inst
48+
49+
instance Multiplicative.orderTop [LE α] : ∀ [OrderTop α], OrderTop (Multiplicative α) :=
50+
fun {inst} => inst
51+
52+
instance Additive.orderTop [LE α] : ∀ [OrderTop α], OrderTop (Additive α) :=
53+
fun {inst} => inst
54+
55+
instance Multiplicative.boundedOrder [LE α] : ∀ [BoundedOrder α], BoundedOrder (Multiplicative α) :=
56+
fun {inst} => inst
57+
58+
instance Additive.boundedOrder [LE α] : ∀ [BoundedOrder α], BoundedOrder (Additive α) :=
59+
fun {inst} => inst
60+
61+
instance Multiplicative.orderedCommMonoid [OrderedAddCommMonoid α] :
62+
OrderedCommMonoid (Multiplicative α) :=
63+
{ Multiplicative.partialOrder, Multiplicative.commMonoid with
64+
mul_le_mul_left := @OrderedAddCommMonoid.add_le_add_left α _ }
65+
66+
instance Additive.orderedAddCommMonoid [OrderedCommMonoid α] :
67+
OrderedAddCommMonoid (Additive α) :=
68+
{ Additive.partialOrder, Additive.addCommMonoid with
69+
add_le_add_left := @OrderedCommMonoid.mul_le_mul_left α _ }
70+
71+
instance Multiplicative.orderedCancelAddCommMonoid [OrderedCancelAddCommMonoid α] :
72+
OrderedCancelCommMonoid (Multiplicative α) :=
73+
{ Multiplicative.orderedCommMonoid with
74+
le_of_mul_le_mul_left := @OrderedCancelAddCommMonoid.le_of_add_le_add_left α _ }
75+
76+
instance Additive.orderedCancelAddCommMonoid [OrderedCancelCommMonoid α] :
77+
OrderedCancelAddCommMonoid (Additive α) :=
78+
{ Additive.orderedAddCommMonoid with
79+
le_of_add_le_add_left := @OrderedCancelCommMonoid.le_of_mul_le_mul_left α _ }
80+
81+
instance Multiplicative.linearOrderedCommMonoid [LinearOrderedAddCommMonoid α] :
82+
LinearOrderedCommMonoid (Multiplicative α) :=
83+
{ Multiplicative.linearOrder, Multiplicative.orderedCommMonoid with }
84+
85+
instance Additive.linearOrderedAddCommMonoid [LinearOrderedCommMonoid α] :
86+
LinearOrderedAddCommMonoid (Additive α) :=
87+
{ Additive.linearOrder, Additive.orderedAddCommMonoid with }
88+
89+
instance Multiplicative.existsMulOfLe [Add α] [LE α] [ExistsAddOfLE α] :
90+
ExistsMulOfLE (Multiplicative α) :=
91+
⟨@exists_add_of_le α _ _ _⟩
92+
93+
instance Additive.existsAddOfLe [Mul α] [LE α] [ExistsMulOfLE α] : ExistsAddOfLE (Additive α) :=
94+
⟨@exists_mul_of_le α _ _ _⟩
95+
96+
instance Multiplicative.canonicallyOrderedMonoid [CanonicallyOrderedAddMonoid α] :
97+
CanonicallyOrderedMonoid (Multiplicative α) :=
98+
{ Multiplicative.orderedCommMonoid, Multiplicative.orderBot,
99+
Multiplicative.existsMulOfLe with le_self_mul := @le_self_add α _ }
100+
101+
instance Additive.canonicallyOrderedAddMonoid [CanonicallyOrderedMonoid α] :
102+
CanonicallyOrderedAddMonoid (Additive α) :=
103+
{ Additive.orderedAddCommMonoid, Additive.orderBot, Additive.existsAddOfLe with
104+
le_self_add := @le_self_mul α _ }
105+
106+
instance Multiplicative.canonicallyLinearOrderedMonoid [CanonicallyLinearOrderedAddMonoid α] :
107+
CanonicallyLinearOrderedMonoid (Multiplicative α) :=
108+
{ Multiplicative.canonicallyOrderedMonoid, Multiplicative.linearOrder with }
109+
110+
instance [CanonicallyLinearOrderedMonoid α] : CanonicallyLinearOrderedAddMonoid (Additive α) :=
111+
{ Additive.canonicallyOrderedAddMonoid, Additive.linearOrder with }
112+
113+
namespace Additive
114+
115+
variable [Preorder α]
116+
117+
@[simp]
118+
theorem ofMul_le {a b : α} : ofMul a ≤ ofMul b ↔ a ≤ b :=
119+
Iff.rfl
120+
#align additive.of_mul_le Additive.ofMul_le
121+
122+
@[simp]
123+
theorem ofMul_lt {a b : α} : ofMul a < ofMul b ↔ a < b :=
124+
Iff.rfl
125+
#align additive.of_mul_lt Additive.ofMul_lt
126+
127+
@[simp]
128+
theorem toMul_le {a b : Additive α} : toMul a ≤ toMul b ↔ a ≤ b :=
129+
Iff.rfl
130+
#align additive.to_mul_le Additive.toMul_le
131+
132+
@[simp]
133+
theorem toMul_lt {a b : Additive α} : toMul a < toMul b ↔ a < b :=
134+
Iff.rfl
135+
#align additive.to_mul_lt Additive.toMul_lt
136+
137+
end Additive
138+
139+
namespace Multiplicative
140+
141+
variable [Preorder α]
142+
143+
@[simp]
144+
theorem ofAdd_le {a b : α} : ofAdd a ≤ ofAdd b ↔ a ≤ b :=
145+
Iff.rfl
146+
#align multiplicative.of_add_le Multiplicative.ofAdd_le
147+
148+
@[simp]
149+
theorem ofAdd_lt {a b : α} : ofAdd a < ofAdd b ↔ a < b :=
150+
Iff.rfl
151+
#align multiplicative.of_add_lt Multiplicative.ofAdd_lt
152+
153+
@[simp]
154+
theorem toAdd_le {a b : Multiplicative α} : toAdd a ≤ toAdd b ↔ a ≤ b :=
155+
Iff.rfl
156+
#align multiplicative.to_add_le Multiplicative.toAdd_le
157+
158+
@[simp]
159+
theorem toAdd_lt {a b : Multiplicative α} : toAdd a < toAdd b ↔ a < b :=
160+
Iff.rfl
161+
#align multiplicative.to_add_lt Multiplicative.toAdd_lt
162+
163+
end Multiplicative

‎Mathlib/Algebra/Order/Monoid/Units.lean‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
/-
2+
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
5+
-/
6+
import Mathlib.Order.Hom.Basic
7+
import Mathlib.Order.MinMax
8+
import Mathlib.Algebra.Group.Units
9+
10+
/-!
11+
# Units in ordered monoids
12+
-/
13+
14+
15+
namespace Units
16+
17+
@[to_additive]
18+
instance [Monoid α] [Preorder α] : Preorder αˣ :=
19+
Preorder.lift val
20+
21+
@[simp, norm_cast, to_additive]
22+
theorem val_le_val [Monoid α] [Preorder α] {a b : αˣ} : (a : α) ≤ b ↔ a ≤ b :=
23+
Iff.rfl
24+
#align units.coe_le_coe Units.val_le_val
25+
26+
@[simp, norm_cast, to_additive]
27+
theorem val_lt_val [Monoid α] [Preorder α] {a b : αˣ} : (a : α) < b ↔ a < b :=
28+
Iff.rfl
29+
#align units.coe_lt_coe Units.val_lt_val
30+
31+
@[to_additive]
32+
instance [Monoid α] [PartialOrder α] : PartialOrder αˣ :=
33+
PartialOrder.lift val Units.ext
34+
35+
@[to_additive]
36+
instance [Monoid α] [LinearOrder α] : LinearOrder αˣ :=
37+
LinearOrder.lift' val Units.ext
38+
39+
/-- `val : αˣ → α` as an order embedding. -/
40+
@[to_additive "`val : add_units α → α` as an order embedding.",
41+
simps (config := { fullyApplied := false })]
42+
def orderEmbeddingVal [Monoid α] [LinearOrder α] : αˣ ↪o α :=
43+
⟨⟨val, ext⟩, Iff.rfl⟩
44+
#align units.order_embedding_coe Units.orderEmbeddingVal
45+
#align add_units.order_embedding_coe AddUnits.orderEmbeddingVal
46+
47+
@[simp, norm_cast, to_additive]
48+
theorem max_val [Monoid α] [LinearOrder α] {a b : αˣ} : (max a b).val = max a.val b.val :=
49+
Monotone.map_max orderEmbeddingVal.monotone
50+
#align units.max_coe Units.max_val
51+
52+
@[simp, norm_cast, to_additive]
53+
theorem min_val [Monoid α] [LinearOrder α] {a b : αˣ} : (min a b).val = min a.val b.val :=
54+
Monotone.map_min orderEmbeddingVal.monotone
55+
#align units.min_coe Units.min_val
56+
57+
end Units

0 commit comments

Comments
 (0)