Skip to content

Commit 6f4600c

Browse files
mattrobballmattrobball
committed
chore (Algebra.Order.Monoid.Unbundled): don't used bundled structured in unbundled (#14351)
Using bundled ordered algebra in `Algebra.Order.Monoid.Unbundled.Pow` seems to defeat the purpose.
1 parent 73d9fbb commit 6f4600c

File tree

10 files changed

+92
-66
lines changed

10 files changed

+92
-66
lines changed

‎Mathlib.lean

+1
Original file line numberDiff line numberDiff line change
@@ -569,6 +569,7 @@ import Mathlib.Algebra.Order.Monoid.TypeTags
569569
import Mathlib.Algebra.Order.Monoid.Unbundled.Basic
570570
import Mathlib.Algebra.Order.Monoid.Unbundled.Defs
571571
import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
572+
import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
572573
import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
573574
import Mathlib.Algebra.Order.Monoid.Units
574575
import Mathlib.Algebra.Order.Monoid.WithTop

‎Mathlib/Algebra/Bounds.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yury G. Kudryashov
55
-/
66
import Mathlib.Algebra.Order.Group.OrderIso
7-
import Mathlib.Algebra.Order.Monoid.OrderDual
87
import Mathlib.Data.Set.Pointwise.Basic
98
import Mathlib.Order.Bounds.OrderIso
109
import Mathlib.Order.ConditionallyCompleteLattice.Basic
10+
import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
1111

1212
#align_import algebra.bounds from "leanprover-community/mathlib"@"dd71334db81d0bd444af1ee339a29298bef40734"
1313

‎Mathlib/Algebra/Order/BigOperators/Group/List.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Yakov Pechersky
55
-/
66
import Mathlib.Algebra.BigOperators.Group.List
77
import Mathlib.Algebra.Order.Monoid.Canonical.Defs
8-
import Mathlib.Algebra.Order.Monoid.OrderDual
8+
import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
99

1010
/-!
1111
# Big operators on a list in ordered groups

‎Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

+1
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ import Mathlib.Algebra.Order.BigOperators.Group.List
88
import Mathlib.Algebra.Order.Group.Abs
99
import Mathlib.Data.List.MinMax
1010
import Mathlib.Data.Multiset.Fold
11+
import Mathlib.Algebra.Order.Monoid.OrderDual
1112

1213
/-!
1314
# Big operators on a multiset in ordered groups

‎Mathlib/Algebra/Order/Group/DenselyOrdered.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
55
-/
66
import Mathlib.Algebra.Order.Monoid.Canonical.Defs
77
import Mathlib.Algebra.Order.Group.Defs
8-
import Mathlib.Algebra.Order.Monoid.OrderDual
8+
import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
99

1010
#align_import algebra.order.group.densely_ordered from "leanprover-community/mathlib"@"4e87c8477c6c38b753f050bc9664b94ee859896c"
1111

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

+1-60
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ 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
-/
66
import Mathlib.Algebra.Order.Group.Synonym
7+
import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
78
import Mathlib.Algebra.Order.Monoid.Defs
89

910
#align_import algebra.order.monoid.order_dual from "leanprover-community/mathlib"@"2258b40dacd2942571c8ce136215350c702dc78f"
@@ -19,66 +20,6 @@ open Function
1920

2021
namespace OrderDual
2122

22-
@[to_additive]
23-
instance contravariantClass_mul_le [LE α] [Mul α] [c : ContravariantClass α α (· * ·) (· ≤ ·)] :
24-
ContravariantClass αᵒᵈ αᵒᵈ (· * ·) (· ≤ ·) :=
25-
⟨c.1.flip⟩
26-
#align order_dual.contravariant_class_add_le OrderDual.contravariantClass_add_le
27-
#align order_dual.contravariant_class_mul_le OrderDual.contravariantClass_mul_le
28-
29-
@[to_additive]
30-
instance covariantClass_mul_le [LE α] [Mul α] [c : CovariantClass α α (· * ·) (· ≤ ·)] :
31-
CovariantClass αᵒᵈ αᵒᵈ (· * ·) (· ≤ ·) :=
32-
⟨c.1.flip⟩
33-
#align order_dual.covariant_class_add_le OrderDual.covariantClass_add_le
34-
#align order_dual.covariant_class_mul_le OrderDual.covariantClass_mul_le
35-
36-
@[to_additive]
37-
instance contravariantClass_swap_mul_le [LE α] [Mul α]
38-
[c : ContravariantClass α α (swap (· * ·)) (· ≤ ·)] :
39-
ContravariantClass αᵒᵈ αᵒᵈ (swap (· * ·)) (· ≤ ·) :=
40-
⟨c.1.flip⟩
41-
#align order_dual.contravariant_class_swap_add_le OrderDual.contravariantClass_swap_add_le
42-
#align order_dual.contravariant_class_swap_mul_le OrderDual.contravariantClass_swap_mul_le
43-
44-
@[to_additive]
45-
instance covariantClass_swap_mul_le [LE α] [Mul α]
46-
[c : CovariantClass α α (swap (· * ·)) (· ≤ ·)] :
47-
CovariantClass αᵒᵈ αᵒᵈ (swap (· * ·)) (· ≤ ·) :=
48-
⟨c.1.flip⟩
49-
#align order_dual.covariant_class_swap_add_le OrderDual.covariantClass_swap_add_le
50-
#align order_dual.covariant_class_swap_mul_le OrderDual.covariantClass_swap_mul_le
51-
52-
@[to_additive]
53-
instance contravariantClass_mul_lt [LT α] [Mul α] [c : ContravariantClass α α (· * ·) (· < ·)] :
54-
ContravariantClass αᵒᵈ αᵒᵈ (· * ·) (· < ·) :=
55-
⟨c.1.flip⟩
56-
#align order_dual.contravariant_class_add_lt OrderDual.contravariantClass_add_lt
57-
#align order_dual.contravariant_class_mul_lt OrderDual.contravariantClass_mul_lt
58-
59-
@[to_additive]
60-
instance covariantClass_mul_lt [LT α] [Mul α] [c : CovariantClass α α (· * ·) (· < ·)] :
61-
CovariantClass αᵒᵈ αᵒᵈ (· * ·) (· < ·) :=
62-
⟨c.1.flip⟩
63-
#align order_dual.covariant_class_add_lt OrderDual.covariantClass_add_lt
64-
#align order_dual.covariant_class_mul_lt OrderDual.covariantClass_mul_lt
65-
66-
@[to_additive]
67-
instance contravariantClass_swap_mul_lt [LT α] [Mul α]
68-
[c : ContravariantClass α α (swap (· * ·)) (· < ·)] :
69-
ContravariantClass αᵒᵈ αᵒᵈ (swap (· * ·)) (· < ·) :=
70-
⟨c.1.flip⟩
71-
#align order_dual.contravariant_class_swap_add_lt OrderDual.contravariantClass_swap_add_lt
72-
#align order_dual.contravariant_class_swap_mul_lt OrderDual.contravariantClass_swap_mul_lt
73-
74-
@[to_additive]
75-
instance covariantClass_swap_mul_lt [LT α] [Mul α]
76-
[c : CovariantClass α α (swap (· * ·)) (· < ·)] :
77-
CovariantClass αᵒᵈ αᵒᵈ (swap (· * ·)) (· < ·) :=
78-
⟨c.1.flip⟩
79-
#align order_dual.covariant_class_swap_add_lt OrderDual.covariantClass_swap_add_lt
80-
#align order_dual.covariant_class_swap_mul_lt OrderDual.covariantClass_swap_mul_lt
81-
8223
@[to_additive]
8324
instance orderedCommMonoid [OrderedCommMonoid α] : OrderedCommMonoid αᵒᵈ :=
8425
{ mul_le_mul_left := fun _ _ h c => mul_le_mul_left' h c }

‎Mathlib/Algebra/Order/Monoid/Unbundled/OrderDual.lean

+82
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
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.Order.Group.Synonym
7+
import Mathlib.Algebra.Order.Monoid.Unbundled.Defs
8+
9+
#align_import algebra.order.monoid.order_dual from "leanprover-community/mathlib"@"2258b40dacd2942571c8ce136215350c702dc78f"
10+
11+
/-! # Unbundled ordered monoid structures on the order dual. -/
12+
13+
14+
universe u
15+
16+
variable {α : Type u}
17+
18+
open Function
19+
20+
namespace OrderDual
21+
22+
@[to_additive]
23+
instance contravariantClass_mul_le [LE α] [Mul α] [c : ContravariantClass α α (· * ·) (· ≤ ·)] :
24+
ContravariantClass αᵒᵈ αᵒᵈ (· * ·) (· ≤ ·) :=
25+
⟨c.1.flip⟩
26+
#align order_dual.contravariant_class_add_le OrderDual.contravariantClass_add_le
27+
#align order_dual.contravariant_class_mul_le OrderDual.contravariantClass_mul_le
28+
29+
@[to_additive]
30+
instance covariantClass_mul_le [LE α] [Mul α] [c : CovariantClass α α (· * ·) (· ≤ ·)] :
31+
CovariantClass αᵒᵈ αᵒᵈ (· * ·) (· ≤ ·) :=
32+
⟨c.1.flip⟩
33+
#align order_dual.covariant_class_add_le OrderDual.covariantClass_add_le
34+
#align order_dual.covariant_class_mul_le OrderDual.covariantClass_mul_le
35+
36+
@[to_additive]
37+
instance contravariantClass_swap_mul_le [LE α] [Mul α]
38+
[c : ContravariantClass α α (swap (· * ·)) (· ≤ ·)] :
39+
ContravariantClass αᵒᵈ αᵒᵈ (swap (· * ·)) (· ≤ ·) :=
40+
⟨c.1.flip⟩
41+
#align order_dual.contravariant_class_swap_add_le OrderDual.contravariantClass_swap_add_le
42+
#align order_dual.contravariant_class_swap_mul_le OrderDual.contravariantClass_swap_mul_le
43+
44+
@[to_additive]
45+
instance covariantClass_swap_mul_le [LE α] [Mul α]
46+
[c : CovariantClass α α (swap (· * ·)) (· ≤ ·)] :
47+
CovariantClass αᵒᵈ αᵒᵈ (swap (· * ·)) (· ≤ ·) :=
48+
⟨c.1.flip⟩
49+
#align order_dual.covariant_class_swap_add_le OrderDual.covariantClass_swap_add_le
50+
#align order_dual.covariant_class_swap_mul_le OrderDual.covariantClass_swap_mul_le
51+
52+
@[to_additive]
53+
instance contravariantClass_mul_lt [LT α] [Mul α] [c : ContravariantClass α α (· * ·) (· < ·)] :
54+
ContravariantClass αᵒᵈ αᵒᵈ (· * ·) (· < ·) :=
55+
⟨c.1.flip⟩
56+
#align order_dual.contravariant_class_add_lt OrderDual.contravariantClass_add_lt
57+
#align order_dual.contravariant_class_mul_lt OrderDual.contravariantClass_mul_lt
58+
59+
@[to_additive]
60+
instance covariantClass_mul_lt [LT α] [Mul α] [c : CovariantClass α α (· * ·) (· < ·)] :
61+
CovariantClass αᵒᵈ αᵒᵈ (· * ·) (· < ·) :=
62+
⟨c.1.flip⟩
63+
#align order_dual.covariant_class_add_lt OrderDual.covariantClass_add_lt
64+
#align order_dual.covariant_class_mul_lt OrderDual.covariantClass_mul_lt
65+
66+
@[to_additive]
67+
instance contravariantClass_swap_mul_lt [LT α] [Mul α]
68+
[c : ContravariantClass α α (swap (· * ·)) (· < ·)] :
69+
ContravariantClass αᵒᵈ αᵒᵈ (swap (· * ·)) (· < ·) :=
70+
⟨c.1.flip⟩
71+
#align order_dual.contravariant_class_swap_add_lt OrderDual.contravariantClass_swap_add_lt
72+
#align order_dual.contravariant_class_swap_mul_lt OrderDual.contravariantClass_swap_mul_lt
73+
74+
@[to_additive]
75+
instance covariantClass_swap_mul_lt [LT α] [Mul α]
76+
[c : CovariantClass α α (swap (· * ·)) (· < ·)] :
77+
CovariantClass αᵒᵈ αᵒᵈ (swap (· * ·)) (· < ·) :=
78+
⟨c.1.flip⟩
79+
#align order_dual.covariant_class_swap_add_lt OrderDual.covariantClass_swap_add_lt
80+
#align order_dual.covariant_class_swap_mul_lt OrderDual.covariantClass_swap_mul_lt
81+
82+

‎Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean

+2-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,8 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jeremy Avigad, Robert Y. Lewis, Yury G. Kudryashov
55
-/
6-
import Mathlib.Algebra.Order.Monoid.OrderDual
6+
import Mathlib.Algebra.Order.Monoid.Unbundled.Basic
7+
import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
78
import Mathlib.Tactic.Lift
89
import Mathlib.Tactic.Monotonicity.Attr
910

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,10 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
66
import Mathlib.Algebra.CharZero.Defs
77
import Mathlib.Algebra.Group.Hom.Defs
88
import Mathlib.Algebra.Order.Monoid.Canonical.Defs
9-
import Mathlib.Algebra.Order.Monoid.OrderDual
109
import Mathlib.Algebra.Order.ZeroLEOne
1110
import Mathlib.Data.Nat.Cast.Defs
1211
import Mathlib.Order.WithBot
12+
import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
1313

1414
#align_import algebra.order.monoid.with_top from "leanprover-community/mathlib"@"0111834459f5d7400215223ea95ae38a1265a907"
1515

‎Mathlib/Order/ConditionallyCompleteLattice/Group.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel
55
-/
66
import Mathlib.Order.ConditionallyCompleteLattice.Basic
77
import Mathlib.Algebra.Order.Group.Defs
8-
import Mathlib.Algebra.Order.Monoid.OrderDual
8+
import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
99

1010
#align_import order.conditionally_complete_lattice.group from "leanprover-community/mathlib"@"46a64b5b4268c594af770c44d9e502afc6a515cb"
1111

0 commit comments

Comments
 (0)