Skip to content

Commit 0d93da5

Browse files
artie2000artie2000
committed
lint
1 parent ffd8243 commit 0d93da5

File tree

2 files changed

+26
-0
lines changed

2 files changed

+26
-0
lines changed

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -97,14 +97,17 @@ some order making the group into a partially ordered group. -/
9797
structure GroupCone (G : Type*) [CommGroup G] extends Submonoid G where
9898
eq_one_of_mem_of_inv_mem' {a} : a ∈ carrier → a⁻¹ ∈ carrier → a = 1
9999

100+
set_option linter.deprecated false in
100101
@[to_additive (attr := deprecated "no replacement" (since := "2026-03-28"))]
101102
instance GroupCone.instSetLike (G : Type*) [CommGroup G] : SetLike (GroupCone G) G where
102103
coe C := C.carrier
103104
coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h
104105

106+
set_option linter.deprecated false in
105107
@[to_additive (attr := deprecated "no replacement" (since := "2026-03-28"))]
106108
instance (G : Type*) [CommGroup G] : PartialOrder (GroupCone G) := .ofSetLike (GroupCone G) G
107109

110+
set_option linter.deprecated false in
108111
@[to_additive (attr := deprecated "no replacement" (since := "2026-03-28"))]
109112
instance GroupCone.instGroupConeClass (G : Type*) [CommGroup G] :
110113
GroupConeClass (GroupCone G) G where
@@ -118,6 +121,7 @@ initialize_simps_projections AddGroupCone (carrier → coe, as_prefix coe)
118121
namespace GroupCone
119122
variable {H : Type*} [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] {a : H}
120123

124+
set_option linter.deprecated false in
121125
variable (H) in
122126
/-- The cone of elements that are at least 1. -/
123127
@[to_additive (attr := deprecated Submonoid.oneLE.isMulPointed (since := "2026-03-28"))
@@ -126,13 +130,19 @@ def oneLE : GroupCone H where
126130
__ := Submonoid.oneLE H
127131
eq_one_of_mem_of_inv_mem' {a} := by simpa using ge_antisymm
128132

133+
set_option linter.deprecated false in
129134
@[to_additive (attr := simp, deprecated "no replacement" (since := "2026-03-28"))]
130135
lemma oneLE_toSubmonoid : (oneLE H).toSubmonoid = .oneLE H := rfl
136+
137+
set_option linter.deprecated false in
131138
@[to_additive (attr := simp, deprecated "no replacement" (since := "2026-03-28"))]
132139
lemma mem_oneLE : a ∈ oneLE H ↔ 1 ≤ a := Iff.rfl
140+
141+
set_option linter.deprecated false in
133142
@[to_additive (attr := simp, norm_cast, deprecated "no replacement" (since := "2026-03-28"))]
134143
lemma coe_oneLE : oneLE H = {x : H | 1 ≤ x} := rfl
135144

145+
set_option linter.deprecated false in
136146
@[to_additive (attr := deprecated Submonoid.oneLE.isMulSpanning (since := "2026-03-28"))]
137147
instance oneLE.hasMemOrInvMem {H : Type*} [CommGroup H] [LinearOrder H] [IsOrderedMonoid H] :
138148
HasMemOrInvMem (oneLE H) where
@@ -142,6 +152,7 @@ end GroupCone
142152

143153
variable {S G : Type*} [CommGroup G] [SetLike S G] (C : S)
144154

155+
set_option linter.deprecated false in
145156
/-- Construct a partial order by designating a cone in an abelian group. -/
146157
@[to_additive (attr := deprecated PartialOrder.mkOfSubmonoid (since := "2026-03-28"))
147158
/-- Construct a partial order by designating a cone in an abelian group. -/]
@@ -152,11 +163,13 @@ abbrev PartialOrder.mkOfGroupCone [GroupConeClass S G] : PartialOrder G where
152163
le_antisymm a b nab nba := by
153164
simpa [div_eq_one, eq_comm] using eq_one_of_mem_of_inv_mem nab (by simpa using nba)
154165

166+
set_option linter.deprecated false in
155167
@[to_additive (attr := simp, deprecated PartialOrder.mkOfSubmonoid_le_iff (since := "2026-03-28"))]
156168
lemma PartialOrder.mkOfGroupCone_le_iff {S G : Type*} [CommGroup G] [SetLike S G]
157169
[GroupConeClass S G] {C : S} {a b : G} :
158170
(mkOfGroupCone C).le a b ↔ b / a ∈ C := Iff.rfl
159171

172+
set_option linter.deprecated false in
160173
/-- Construct a linear order by designating a maximal cone in an abelian group. -/
161174
@[to_additive (attr := deprecated LinearOrder.mkOfSubmonoid (since := "2026-03-28"))
162175
/-- Construct a linear order by designating a maximal cone in an abelian group. -/]
@@ -166,6 +179,7 @@ abbrev LinearOrder.mkOfGroupCone
166179
le_total a b := by simpa using mem_or_inv_mem C (b / a)
167180
toDecidableLE _ := _
168181

182+
set_option linter.deprecated false in
169183
/-- Construct a partially ordered abelian group by designating a cone in an abelian group. -/
170184
@[to_additive (attr := deprecated IsOrderedMonoid.mkOfSubmonoid (since := "2026-03-28"))
171185
/-- Construct a partially ordered abelian group by designating a cone in an abelian group. -/]

‎Mathlib/Algebra/Order/Ring/Cone.lean‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,11 +36,13 @@ theorem IsOrderedRing.mkOfSubsemiring :
3636
haveI : ZeroLEOneClass R := ⟨by simp⟩
3737
.of_mul_nonneg fun x y xnn ynn ↦ show _ ∈ S by simpa using Subsemiring.mul_mem _ xnn ynn
3838

39+
set_option linter.deprecated false in
3940
/-- `RingConeClass S R` says that `S` is a type of cones in `R`. -/
4041
@[deprecated "Unbundled to `AddSubmonoid.IsPointed`" (since := "2026-03-28")]
4142
class RingConeClass (S : Type*) (R : outParam Type*) [Ring R] [SetLike S R] : Prop
4243
extends AddGroupConeClass S R, SubsemiringClass S R
4344

45+
set_option linter.deprecated false in
4446
/-- A (positive) cone in a ring is a subsemiring that
4547
does not contain both `a` and `-a` for any nonzero `a`.
4648
This is equivalent to being the set of non-negative elements of
@@ -51,14 +53,17 @@ structure RingCone (R : Type*) [Ring R] extends Subsemiring R, AddGroupCone R
5153
/-- Interpret a cone in a ring as a cone in the underlying additive group. -/
5254
add_decl_doc RingCone.toAddGroupCone
5355

56+
set_option linter.deprecated false in
5457
@[deprecated "no replacement" (since := "2026-03-28")]
5558
instance RingCone.instSetLike (R : Type*) [Ring R] : SetLike (RingCone R) R where
5659
coe C := C.carrier
5760
coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h
5861

62+
set_option linter.deprecated false in
5963
@[deprecated "no replacement" (since := "2026-03-28")]
6064
instance (R : Type*) [Ring R] : PartialOrder (RingCone R) := .ofSetLike (RingCone R) R
6165

66+
set_option linter.deprecated false in
6267
@[deprecated "no replacement" (since := "2026-03-28")]
6368
instance RingCone.instRingConeClass (R : Type*) [Ring R] :
6469
RingConeClass (RingCone R) R where
@@ -82,25 +87,31 @@ namespace RingCone
8287

8388
variable {T : Type*} [Ring T] [PartialOrder T] [IsOrderedRing T] {a : T}
8489

90+
set_option linter.deprecated false in
8591
variable (T) in
8692
/-- Construct a cone from the set of non-negative elements of a partially ordered ring. -/
8793
@[deprecated Subsemiring.nonneg.isPointed (since := "2026-03-28")]
8894
def nonneg : RingCone T where
8995
__ := Subsemiring.nonneg T
9096
eq_zero_of_mem_of_neg_mem' {a} := by simpa using ge_antisymm
9197

98+
set_option linter.deprecated false in
9299
@[simp, deprecated "no replacement" (since := "2026-03-28")]
93100
lemma nonneg_toSubsemiring : (nonneg T).toSubsemiring = .nonneg T := rfl
94101

102+
set_option linter.deprecated false in
95103
@[simp, deprecated "no replacement" (since := "2026-03-28")]
96104
lemma nonneg_toAddGroupCone : (nonneg T).toAddGroupCone = .nonneg T := rfl
97105

106+
set_option linter.deprecated false in
98107
@[simp, deprecated "no replacement" (since := "2026-03-28")]
99108
lemma mem_nonneg : a ∈ nonneg T ↔ 0 ≤ a := Iff.rfl
100109

110+
set_option linter.deprecated false in
101111
@[simp, deprecated "no replacement" (since := "2026-03-28")]
102112
lemma coe_nonneg : nonneg T = {x : T | 0 ≤ x} := rfl
103113

114+
set_option linter.deprecated false in
104115
@[deprecated Subsemiring.nonneg.isSpanning (since := "2026-03-28")]
105116
instance nonneg.hasMemOrNegMem {T : Type*} [Ring T] [LinearOrder T] [IsOrderedRing T] :
106117
HasMemOrNegMem (nonneg T) where
@@ -110,6 +121,7 @@ end RingCone
110121

111122
variable {S R : Type*} [Ring R] [SetLike S R] (C : S)
112123

124+
set_option linter.deprecated false in
113125
/-- Construct a partially ordered ring by designating a cone in a ring. -/
114126
@[deprecated IsOrderedRing.mkOfSubsemiring (since := "2026-03-28")]
115127
lemma IsOrderedRing.mkOfCone [RingConeClass S R] :

0 commit comments

Comments
 (0)