Skip to content

Commit fd6ea04

Browse files
YaelDilliesYaelDillies
committed
feat: characterise regular elements of type synonyms (#31739)
1 parent 6002bc1 commit fd6ea04

File tree

5 files changed

+186
-21
lines changed

5 files changed

+186
-21
lines changed

‎Mathlib/Algebra/Group/TypeTags/Basic.lean‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -288,6 +288,56 @@ theorem ofAdd_nsmul [AddMonoid α] (n : ℕ) (a : α) : ofAdd (n • a) = ofAdd
288288
theorem toAdd_pow [AddMonoid α] (a : Multiplicative α) (n : ℕ) : (a ^ n).toAdd = n • a.toAdd :=
289289
rfl
290290

291+
section Monoid
292+
variable [Monoid α]
293+
294+
@[simp]
295+
lemma isAddLeftRegular_ofMul {a : α} : IsAddLeftRegular (Additive.ofMul a) ↔ IsLeftRegular a := .rfl
296+
297+
@[simp]
298+
lemma isLeftRegular_toMul {a : Additive α} : IsLeftRegular a.toMul ↔ IsAddLeftRegular a := .rfl
299+
300+
@[simp]
301+
lemma isAddRightRegular_ofMul {a : α} : IsAddRightRegular (Additive.ofMul a) ↔ IsRightRegular a :=
302+
.rfl
303+
304+
@[simp]
305+
lemma isRightRegular_toMul {a : Additive α} : IsRightRegular a.toMul ↔ IsAddRightRegular a := .rfl
306+
307+
@[simp] lemma isAddRegular_ofMul {a : α} : IsAddRegular (Additive.ofMul a) ↔ IsRegular a := by
308+
simp [isAddRegular_iff, isRegular_iff]
309+
310+
@[simp] lemma isRegular_toMul {a : Additive α} : IsRegular a.toMul ↔ IsAddRegular a := by
311+
simp [isAddRegular_iff, isRegular_iff]
312+
313+
end Monoid
314+
315+
section AddMonoid
316+
variable [AddMonoid α]
317+
318+
@[simp]
319+
lemma isLeftRegular_ofAdd {a : α} : IsLeftRegular (Multiplicative.ofAdd a) ↔ IsAddLeftRegular a :=
320+
.rfl
321+
322+
@[simp]
323+
lemma isAddLeftRegular_toAdd {a : Multiplicative α} : IsAddLeftRegular a.toAdd ↔ IsLeftRegular a :=
324+
.rfl
325+
326+
@[simp]
327+
lemma isRightRegular_ofAdd {a : α} :
328+
IsRightRegular (Multiplicative.ofAdd a) ↔ IsAddRightRegular a := .rfl
329+
330+
@[simp] lemma isAddRightRegular_toAdd {a : Multiplicative α} :
331+
IsAddRightRegular a.toAdd ↔ IsRightRegular a := .rfl
332+
333+
@[simp] lemma isRegular_ofAdd {a : α} : IsRegular (Multiplicative.ofAdd a) ↔ IsAddRegular a := by
334+
simp [isAddRegular_iff, isRegular_iff]
335+
336+
@[simp] lemma isAddRegular_toAdd {a : Multiplicative α} : IsAddRegular a.toAdd ↔ IsRegular a := by
337+
simp [isAddRegular_iff, isRegular_iff]
338+
339+
end AddMonoid
340+
291341
instance Additive.addLeftCancelMonoid [LeftCancelMonoid α] : AddLeftCancelMonoid (Additive α) :=
292342
{ Additive.addMonoid, Additive.addLeftCancelSemigroup with }
293343

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

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,9 @@ theorem toDual_one [One α] : toDual (1 : α) = 1 := rfl
104104
@[to_additive (attr := simp)]
105105
theorem ofDual_one [One α] : (ofDual 1 : α) = 1 := rfl
106106

107+
@[to_additive (attr := simp)] lemma toDual_eq_one [One α] {a : α} : toDual a = 1 ↔ a = 1 := .rfl
108+
@[to_additive (attr := simp)] lemma ofDual_eq_one [One α] {a : αᵒᵈ} : ofDual a = 1 ↔ a = 1 := .rfl
109+
107110
@[to_additive (attr := simp)]
108111
theorem toDual_mul [Mul α] (a b : α) : toDual (a * b) = toDual a * toDual b := rfl
109112

@@ -134,6 +137,29 @@ theorem pow_toDual [Pow α β] (a : α) (b : β) : a ^ toDual b = a ^ b := rfl
134137
@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) ofDual_smul']
135138
theorem pow_ofDual [Pow α β] (a : α) (b : βᵒᵈ) : a ^ ofDual b = a ^ b := rfl
136139

140+
section Monoid
141+
variable [Monoid α]
142+
143+
@[to_additive (attr := simp)]
144+
lemma isLeftRegular_toDual {a : α} : IsLeftRegular (toDual a) ↔ IsLeftRegular a := .rfl
145+
146+
@[to_additive (attr := simp)]
147+
lemma isLeftRegular_ofDual {a : αᵒᵈ} : IsLeftRegular (ofDual a) ↔ IsLeftRegular a := .rfl
148+
149+
@[to_additive (attr := simp)]
150+
lemma isRightRegular_toDual {a : α} : IsRightRegular (toDual a) ↔ IsRightRegular a := .rfl
151+
152+
@[to_additive (attr := simp)]
153+
lemma isRightRegular_ofDual {a : αᵒᵈ} : IsRightRegular (ofDual a) ↔ IsRightRegular a := .rfl
154+
155+
@[to_additive (attr := simp)]
156+
lemma isRegular_toDual {a : α} : IsRegular (toDual a) ↔ IsRegular a := .rfl
157+
158+
@[to_additive (attr := simp)]
159+
lemma isRegular_ofDual {a : αᵒᵈ} : IsRegular (ofDual a) ↔ IsRegular a := .rfl
160+
161+
end Monoid
162+
137163
/-! ### Lexicographical order -/
138164

139165

@@ -260,6 +286,29 @@ theorem pow_toLex [Pow α β] (a : α) (b : β) : a ^ toLex b = a ^ b := rfl
260286
@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) ofLex_smul']
261287
theorem pow_ofLex [Pow α β] (a : α) (b : Lex β) : a ^ ofLex b = a ^ b := rfl
262288

289+
section Monoid
290+
variable [Monoid α]
291+
292+
@[to_additive (attr := simp)]
293+
lemma isLeftRegular_toLex {a : α} : IsLeftRegular (toLex a) ↔ IsLeftRegular a := .rfl
294+
295+
@[to_additive (attr := simp)]
296+
lemma isLeftRegular_ofLex {a : Lex α} : IsLeftRegular (ofLex a) ↔ IsLeftRegular a := .rfl
297+
298+
@[to_additive (attr := simp)]
299+
lemma isRightRegular_toLex {a : α} : IsRightRegular (toLex a) ↔ IsRightRegular a := .rfl
300+
301+
@[to_additive (attr := simp)]
302+
lemma isRightRegular_ofLex {a : Lex α} : IsRightRegular (ofLex a) ↔ IsRightRegular a := .rfl
303+
304+
@[to_additive (attr := simp)]
305+
lemma isRegular_toLex {a : α} : IsRegular (toLex a) ↔ IsRegular a := .rfl
306+
307+
@[to_additive (attr := simp)]
308+
lemma isRegular_ofLex {a : Lex α} : IsRegular (ofLex a) ↔ IsRegular a := .rfl
309+
310+
end Monoid
311+
263312
/-! ### Colexicographical order -/
264313

265314

@@ -385,3 +434,26 @@ theorem pow_toColex [Pow α β] (a : α) (b : β) : a ^ toColex b = a ^ b := rfl
385434

386435
@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) ofColex_smul']
387436
theorem pow_ofColex [Pow α β] (a : α) (b : Colex β) : a ^ ofColex b = a ^ b := rfl
437+
438+
section Monoid
439+
variable [Monoid α]
440+
441+
@[to_additive (attr := simp)]
442+
lemma isLeftRegular_toColex {a : α} : IsLeftRegular (toColex a) ↔ IsLeftRegular a := .rfl
443+
444+
@[to_additive (attr := simp)]
445+
lemma isLeftRegular_ofColex {a : Colex α} : IsLeftRegular (ofColex a) ↔ IsLeftRegular a := .rfl
446+
447+
@[to_additive (attr := simp)]
448+
lemma isRightRegular_toColex {a : α} : IsRightRegular (toColex a) ↔ IsRightRegular a := .rfl
449+
450+
@[to_additive (attr := simp)]
451+
lemma isRightRegular_ofColex {a : Colex α} : IsRightRegular (ofColex a) ↔ IsRightRegular a := .rfl
452+
453+
@[to_additive (attr := simp)]
454+
lemma isRegular_toColex {a : α} : IsRegular (toColex a) ↔ IsRegular a := .rfl
455+
456+
@[to_additive (attr := simp)]
457+
lemma isRegular_ofColex {a : Colex α} : IsRegular (ofColex a) ↔ IsRegular a := .rfl
458+
459+
end Monoid

‎Mathlib/Algebra/Order/GroupWithZero/Canonical.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -206,15 +206,15 @@ instance instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual
206206
mul_zero := @add_top _ (_)
207207
zero_le_one := (le_top : (0 : α) ≤ ⊤)
208208

209-
@[simp]
209+
@[deprecated "Use simp" (since := "2025-11-17")]
210210
theorem ofAdd_toDual_eq_zero_iff [LinearOrderedAddCommMonoidWithTop α]
211211
(x : α) : Multiplicative.ofAdd (OrderDual.toDual x) = 0 ↔ x = ⊤ := Iff.rfl
212212

213-
@[simp]
213+
@[deprecated "Use simp" (since := "2025-11-17")]
214214
theorem ofDual_toAdd_eq_top_iff [LinearOrderedAddCommMonoidWithTop α]
215215
(x : Multiplicative αᵒᵈ) : OrderDual.ofDual x.toAdd = ⊤ ↔ x = 0 := Iff.rfl
216216

217-
@[simp]
217+
@[deprecated bot_eq_zero'' (since := "2025-11-17")]
218218
theorem ofAdd_bot [LinearOrderedAddCommMonoidWithTop α] :
219219
Multiplicative.ofAdd ⊥ = (0 : Multiplicative αᵒᵈ) := rfl
220220

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

Lines changed: 52 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ instance Additive.existsAddOfLe [Mul α] [LE α] [ExistsMulOfLE α] : ExistsAddO
6767
⟨@exists_mul_of_le α _ _ _⟩
6868

6969
namespace Additive
70-
70+
section Preorder
7171
variable [Preorder α]
7272

7373
@[simp]
@@ -89,12 +89,37 @@ theorem toMul_lt {a b : Additive α} : a.toMul < b.toMul ↔ a < b :=
8989
@[gcongr] alias ⟨_, toMul_mono⟩ := toMul_le
9090
@[gcongr] alias ⟨_, ofMul_mono⟩ := ofMul_le
9191
@[gcongr] alias ⟨_, toMul_strictMono⟩ := toMul_lt
92-
@[gcongr] alias ⟨_, foMul_strictMono⟩ := ofMul_lt
92+
@[gcongr] alias ⟨_, ofMul_strictMono⟩ := ofMul_lt
93+
94+
@[deprecated (since := "2025-11-18")] alias foMul_strictMono := ofMul_strictMono
95+
96+
end Preorder
97+
98+
section OrderTop
99+
variable [LE α] [OrderTop α]
100+
101+
@[simp] lemma ofMul_top : ofMul (⊤ : α) = ⊤ := rfl
102+
@[simp] lemma toMul_top : toMul ⊤ = (⊤ : α) := rfl
103+
104+
@[simp] lemma ofMul_eq_top {a : α} : ofMul a = ⊤ ↔ a = ⊤ := .rfl
105+
@[simp] lemma toMul_eq_top {a : Additive α} : toMul a = ⊤ ↔ a = ⊤ := .rfl
106+
107+
end OrderTop
108+
109+
section OrderBot
110+
variable [LE α] [OrderBot α]
111+
112+
@[simp] lemma ofMul_bot : ofMul (⊥ : α) = ⊥ := rfl
113+
@[simp] lemma toMul_bot : toMul ⊥ = (⊥ : α) := rfl
114+
115+
@[simp] lemma ofMul_eq_bot {a : α} : ofMul a = ⊥ ↔ a = ⊥ := .rfl
116+
@[simp] lemma toMul_eq_bot {a : Additive α} : toMul a = ⊥ ↔ a = ⊥ := .rfl
93117

118+
end OrderBot
94119
end Additive
95120

96121
namespace Multiplicative
97-
122+
section Preorder
98123
variable [Preorder α]
99124

100125
@[simp]
@@ -118,4 +143,28 @@ theorem toAdd_lt {a b : Multiplicative α} : a.toAdd < b.toAdd ↔ a < b :=
118143
@[gcongr] alias ⟨_, toAdd_strictMono⟩ := toAdd_lt
119144
@[gcongr] alias ⟨_, ofAdd_strictMono⟩ := ofAdd_lt
120145

146+
end Preorder
147+
148+
section OrderTop
149+
variable [LE α] [OrderTop α]
150+
151+
@[simp] lemma ofAdd_top : ofAdd (⊤ : α) = ⊤ := rfl
152+
@[simp] lemma toAdd_top : toAdd ⊤ = (⊤ : α) := rfl
153+
154+
@[simp] lemma ofAdd_eq_top {a : α} : ofAdd a = ⊤ ↔ a = ⊤ := .rfl
155+
@[simp] lemma toAdd_eq_top {a : Multiplicative α} : toAdd a = ⊤ ↔ a = ⊤ := .rfl
156+
157+
end OrderTop
158+
159+
section OrderBot
160+
variable [LE α] [OrderBot α]
161+
162+
@[simp] lemma ofAdd_bot : ofAdd (⊥ : α) = ⊥ := rfl
163+
@[simp] lemma toAdd_bot : toAdd ⊥ = (⊥ : α) := rfl
164+
165+
@[simp] lemma ofAdd_eq_bot {a : α} : ofAdd a = ⊥ ↔ a = ⊥ := .rfl
166+
@[simp] lemma toAdd_eq_bot {a : Multiplicative α} : toAdd a = ⊥ ↔ a = ⊥ := .rfl
167+
168+
end OrderBot
169+
121170
end Multiplicative

‎Mathlib/Order/BoundedOrder/Basic.lean‎

Lines changed: 9 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -227,21 +227,15 @@ instance instOrderBot [LE α] [OrderTop α] : OrderBot αᵒᵈ where
227227
__ := inferInstanceAs (Bot αᵒᵈ)
228228
bot_le := @le_top α _ _
229229

230-
@[simp]
231-
theorem ofDual_bot [Top α] : ofDual ⊥ = (⊤ : α) :=
232-
rfl
233-
234-
@[simp]
235-
theorem ofDual_top [Bot α] : ofDual ⊤ = (⊥ : α) :=
236-
rfl
237-
238-
@[simp]
239-
theorem toDual_bot [Bot α] : toDual (⊥ : α) = ⊤ :=
240-
rfl
241-
242-
@[simp]
243-
theorem toDual_top [Top α] : toDual (⊤ : α) = ⊥ :=
244-
rfl
230+
@[simp] lemma ofDual_bot [Top α] : ofDual ⊥ = (⊤ : α) := rfl
231+
@[simp] lemma ofDual_top [Bot α] : ofDual ⊤ = (⊥ : α) := rfl
232+
@[simp] lemma toDual_bot [Bot α] : toDual (⊥ : α) = ⊤ := rfl
233+
@[simp] lemma toDual_top [Top α] : toDual (⊤ : α) = ⊥ := rfl
234+
235+
@[simp] lemma ofDual_eq_bot [Bot α] {a : αᵒᵈ} : ofDual a = ⊥ ↔ a = ⊤ := .rfl
236+
@[simp] lemma ofDual_eq_top [Top α] {a : αᵒᵈ} : ofDual a = ⊤ ↔ a = ⊥ := .rfl
237+
@[simp] lemma toDual_eq_bot [Top α] {a : α} : toDual a = ⊥ ↔ a = ⊤ := .rfl
238+
@[simp] lemma toDual_eq_top [Bot α] {a : α} : toDual a = ⊤ ↔ a = ⊥ := .rfl
245239

246240
end OrderDual
247241

0 commit comments

Comments
 (0)