Skip to content

Commit 121243a

Browse files
urkudurkud
committed
chore(Normed/Field/UnitBall): review instances (#24188)
1 parent 4ecf18c commit 121243a

File tree

5 files changed

+160
-60
lines changed

5 files changed

+160
-60
lines changed

β€ŽMathlib/Analysis/Complex/Circle.leanβ€Ž

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ variable {x y : Circle}
5353

5454
instance instCoeOut : CoeOut Circle β„‚ := subtypeCoe
5555

56-
instance instCommGroup : CommGroup Circle := Metric.sphere.commGroup
56+
instance instCommGroup : CommGroup Circle := Metric.sphere.instCommGroup
5757
instance instMetricSpace : MetricSpace Circle := Subtype.metricSpace
5858

5959
@[ext] lemma ext : (x : β„‚) = y β†’ x = y := Subtype.ext
@@ -93,7 +93,7 @@ def toUnits : Circle β†’* Units β„‚ := unitSphereToUnits β„‚
9393
@[simp] lemma toUnits_apply (z : Circle) : toUnits z = Units.mk0 ↑z z.coe_ne_zero := rfl
9494

9595
instance : CompactSpace Circle := Metric.sphere.compactSpace _ _
96-
instance : IsTopologicalGroup Circle := Metric.sphere.topologicalGroup
96+
instance : IsTopologicalGroup Circle := Metric.sphere.instIsTopologicalGroup
9797
instance instUniformSpace : UniformSpace Circle := instUniformSpaceSubtype
9898
instance : IsUniformGroup Circle := by
9999
convert topologicalGroup_is_uniform_of_compactSpace Circle

β€ŽMathlib/Analysis/Complex/UnitDisc/Basic.leanβ€Ž

Lines changed: 12 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -31,13 +31,21 @@ open UnitDisc
3131

3232
namespace UnitDisc
3333

34+
/-- Coercion to `β„‚`. -/
35+
@[coe] protected def coe : 𝔻 β†’ β„‚ := Subtype.val
36+
3437
instance instCommSemigroup : CommSemigroup UnitDisc := by unfold UnitDisc; infer_instance
38+
instance instSemigroupWithZero : SemigroupWithZero UnitDisc := by unfold UnitDisc; infer_instance
39+
instance instIsCancelMulZero : IsCancelMulZero UnitDisc := by unfold UnitDisc; infer_instance
3540
instance instHasDistribNeg : HasDistribNeg UnitDisc := by unfold UnitDisc; infer_instance
36-
instance instCoe : Coe UnitDisc β„‚ := ⟨Subtype.val⟩
41+
instance instCoe : Coe UnitDisc β„‚ := ⟨UnitDisc.coe⟩
3742

3843
theorem coe_injective : Injective ((↑) : 𝔻 β†’ β„‚) :=
3944
Subtype.coe_injective
4045

46+
@[simp, norm_cast]
47+
theorem coe_inj {z w : 𝔻} : (z : β„‚) = w ↔ z = w := Subtype.val_inj
48+
4149
theorem norm_lt_one (z : 𝔻) : β€–(z : β„‚)β€– < 1 :=
4250
mem_ball_zero_iff.1 z.2
4351

@@ -81,12 +89,6 @@ theorem mk_coe (z : 𝔻) (hz : β€–(z : β„‚)β€– < 1 := z.norm_lt_one) : mk z hz
8189
theorem mk_neg (z : β„‚) (hz : β€–-zβ€– < 1) : mk (-z) hz = -mk z (norm_neg z β–Έ hz) :=
8290
rfl
8391

84-
instance : SemigroupWithZero 𝔻 :=
85-
{ instCommSemigroup with
86-
zero := mk 0 <| norm_zero.trans_lt one_pos
87-
zero_mul := fun _ => coe_injective <| zero_mul _
88-
mul_zero := fun _ => coe_injective <| mul_zero _ }
89-
9092
@[simp]
9193
theorem coe_zero : ((0 : 𝔻) : β„‚) = 0 :=
9294
rfl
@@ -95,6 +97,9 @@ theorem coe_zero : ((0 : 𝔻) : β„‚) = 0 :=
9597
theorem coe_eq_zero {z : 𝔻} : (z : β„‚) = 0 ↔ z = 0 :=
9698
coe_injective.eq_iff' coe_zero
9799

100+
@[simp] theorem mk_zero : mk 0 (by simp) = 0 := rfl
101+
@[simp] theorem mk_eq_zero {z : β„‚} (hz : β€–zβ€– < 1) : mk z hz = 0 ↔ z = 0 := by simp [← coe_inj]
102+
98103
instance : Inhabited 𝔻 :=
99104
⟨0⟩
100105

β€ŽMathlib/Analysis/Fourier/AddCircle.leanβ€Ž

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -170,7 +170,8 @@ theorem fourier_norm [Fact (0 < T)] (n : β„€) : β€–@fourier T nβ€– = 1 := by
170170
/-- For `n β‰  0`, a translation by `T / 2 / n` negates the function `fourier n`. -/
171171
theorem fourier_add_half_inv_index {n : β„€} (hn : n β‰  0) (hT : 0 < T) (x : AddCircle T) :
172172
@fourier T n (x + ↑(T / 2 / n)) = -fourier n x := by
173-
rw [fourier_apply, zsmul_add, ← QuotientAddGroup.mk_zsmul, toCircle_add, coe_mul_unitSphere]
173+
rw [fourier_apply, zsmul_add, ← QuotientAddGroup.mk_zsmul, toCircle_add,
174+
Metric.unitSphere.coe_mul]
174175
have : (n : β„‚) β‰  0 := by simpa using hn
175176
have : (@toCircle T (n β€’ (T / 2 / n) : ℝ) : β„‚) = -1 := by
176177
rw [zsmul_eq_mul, toCircle, Function.Periodic.lift_coe, Circle.coe_exp]

β€ŽMathlib/Analysis/Fourier/BoundedContinuousFunctionChar.leanβ€Ž

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ theorem ext_of_char_eq (he : Continuous e) (he' : e β‰  1)
8383
obtain ⟨a, ha⟩ := DFunLike.ne_iff.mp he'
8484
use (a / (L (v - v') w)) β€’ w
8585
simp only [map_sub, LinearMap.sub_apply, char_apply, ne_eq]
86-
rw [← div_eq_one_iff_eq (Circle.coe_ne_zero _), div_eq_inv_mul, ← coe_inv_unitSphere,
86+
rw [← div_eq_one_iff_eq (Circle.coe_ne_zero _), div_eq_inv_mul, ← Metric.unitSphere.coe_inv,
8787
← e.map_neg_eq_inv, ← Submonoid.coe_mul, ← e.map_add_eq_mul, OneMemClass.coe_eq_one]
8888
calc e (- L v' ((a / (L v w - L v' w)) β€’ w) + L v ((a / (L v w - L v' w)) β€’ w))
8989
_ = e (- (a / (L v w - L v' w)) β€’ L v' w + (a / (L v w - L v' w)) β€’ L v w) := by

β€ŽMathlib/Analysis/Normed/Field/UnitBall.leanβ€Ž

Lines changed: 143 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -20,80 +20,165 @@ open Set Metric
2020

2121
variable {π•œ : Type*}
2222

23+
/-!
24+
### Algebraic structures on `Metric.ball 0 1`
25+
-/
26+
2327
/-- Unit ball in a non-unital seminormed ring as a bundled `Subsemigroup`. -/
2428
def Subsemigroup.unitBall (π•œ : Type*) [NonUnitalSeminormedRing π•œ] : Subsemigroup π•œ where
2529
carrier := ball (0 : π•œ) 1
2630
mul_mem' hx hy := by
2731
rw [mem_ball_zero_iff] at *
2832
exact (norm_mul_le _ _).trans_lt (mul_lt_one_of_nonneg_of_lt_one_left (norm_nonneg _) hx hy.le)
2933

30-
instance Metric.unitBall.semigroup [NonUnitalSeminormedRing π•œ] : Semigroup (ball (0 : π•œ) 1) :=
34+
instance Metric.unitBall.instSemigroup [NonUnitalSeminormedRing π•œ] : Semigroup (ball (0 : π•œ) 1) :=
3135
MulMemClass.toSemigroup (Subsemigroup.unitBall π•œ)
3236

33-
instance Metric.unitBall.continuousMul [NonUnitalSeminormedRing π•œ] :
37+
instance Metric.unitBall.instContinuousMul [NonUnitalSeminormedRing π•œ] :
3438
ContinuousMul (ball (0 : π•œ) 1) :=
3539
(Subsemigroup.unitBall π•œ).continuousMul
3640

37-
instance Metric.unitBall.commSemigroup [SeminormedCommRing π•œ] : CommSemigroup (ball (0 : π•œ) 1) :=
41+
instance Metric.unitBall.instCommSemigroup [SeminormedCommRing π•œ] :
42+
CommSemigroup (ball (0 : π•œ) 1) :=
3843
MulMemClass.toCommSemigroup (Subsemigroup.unitBall π•œ)
3944

40-
instance Metric.unitBall.hasDistribNeg [NonUnitalSeminormedRing π•œ] :
45+
instance Metric.unitBall.instHasDistribNeg [NonUnitalSeminormedRing π•œ] :
4146
HasDistribNeg (ball (0 : π•œ) 1) :=
4247
Subtype.coe_injective.hasDistribNeg ((↑) : ball (0 : π•œ) 1 β†’ π•œ) (fun _ => rfl) fun _ _ => rfl
4348

4449
@[simp, norm_cast]
45-
theorem coe_mul_unitBall [NonUnitalSeminormedRing π•œ] (x y : ball (0 : π•œ) 1) :
50+
protected theorem Metric.unitBall.coe_mul [NonUnitalSeminormedRing π•œ] (x y : ball (0 : π•œ) 1) :
4651
↑(x * y) = (x * y : π•œ) :=
4752
rfl
4853

54+
@[deprecated (since := "2025-04-18")]
55+
alias coe_mul_unitBall := Metric.unitBall.coe_mul
56+
57+
instance Metric.unitBall.instZero [Zero π•œ] [PseudoMetricSpace π•œ] : Zero (ball (0 : π•œ) 1) :=
58+
⟨⟨0, by simp⟩⟩
59+
60+
@[simp, norm_cast]
61+
protected theorem Metric.unitBall.coe_zero [Zero π•œ] [PseudoMetricSpace π•œ] :
62+
((0 : ball (0 : π•œ) 1) : π•œ) = 0 :=
63+
rfl
64+
65+
@[simp, norm_cast]
66+
protected theorem Metric.unitBall.coe_eq_zero [Zero π•œ] [PseudoMetricSpace π•œ] {a : ball (0 : π•œ) 1} :
67+
(a : π•œ) = 0 ↔ a = 0 :=
68+
Subtype.val_injective.eq_iff' unitBall.coe_zero
69+
70+
instance Metric.unitBall.instSemigroupWithZero [NonUnitalSeminormedRing π•œ] :
71+
SemigroupWithZero (ball (0 : π•œ) 1) where
72+
zero_mul _ := Subtype.eq <| zero_mul _
73+
mul_zero _ := Subtype.eq <| mul_zero _
74+
75+
instance Metric.unitBall.instIsLeftCancelMulZero [NonUnitalSeminormedRing π•œ]
76+
[IsLeftCancelMulZero π•œ] : IsLeftCancelMulZero (ball (0 : π•œ) 1) :=
77+
Subtype.val_injective.isLeftCancelMulZero _ rfl fun _ _ ↦ rfl
78+
79+
instance Metric.unitBall.instIsRightCancelMulZero [NonUnitalSeminormedRing π•œ]
80+
[IsRightCancelMulZero π•œ] : IsRightCancelMulZero (ball (0 : π•œ) 1) :=
81+
Subtype.val_injective.isRightCancelMulZero _ rfl fun _ _ ↦ rfl
82+
83+
instance Metric.unitBall.instIsCancelMulZero [NonUnitalSeminormedRing π•œ]
84+
[IsCancelMulZero π•œ] : IsCancelMulZero (ball (0 : π•œ) 1) where
85+
86+
/-!
87+
### Algebraic instances for `Metric.closedBall 0 1`
88+
-/
89+
4990
/-- Closed unit ball in a non-unital seminormed ring as a bundled `Subsemigroup`. -/
5091
def Subsemigroup.unitClosedBall (π•œ : Type*) [NonUnitalSeminormedRing π•œ] : Subsemigroup π•œ where
5192
carrier := closedBall 0 1
5293
mul_mem' hx hy := by
5394
rw [mem_closedBall_zero_iff] at *
5495
exact (norm_mul_le _ _).trans (mul_le_oneβ‚€ hx (norm_nonneg _) hy)
5596

56-
instance Metric.unitClosedBall.semigroup [NonUnitalSeminormedRing π•œ] :
97+
instance Metric.unitClosedBall.instSemigroup [NonUnitalSeminormedRing π•œ] :
5798
Semigroup (closedBall (0 : π•œ) 1) :=
5899
MulMemClass.toSemigroup (Subsemigroup.unitClosedBall π•œ)
59100

60-
instance Metric.unitClosedBall.hasDistribNeg [NonUnitalSeminormedRing π•œ] :
101+
instance Metric.unitClosedBall.instHasDistribNeg [NonUnitalSeminormedRing π•œ] :
61102
HasDistribNeg (closedBall (0 : π•œ) 1) :=
62103
Subtype.coe_injective.hasDistribNeg ((↑) : closedBall (0 : π•œ) 1 β†’ π•œ) (fun _ => rfl) fun _ _ => rfl
63104

64-
instance Metric.unitClosedBall.continuousMul [NonUnitalSeminormedRing π•œ] :
105+
instance Metric.unitClosedBall.instContinuousMul [NonUnitalSeminormedRing π•œ] :
65106
ContinuousMul (closedBall (0 : π•œ) 1) :=
66107
(Subsemigroup.unitClosedBall π•œ).continuousMul
67108

68109
@[simp, norm_cast]
69-
theorem coe_mul_unitClosedBall [NonUnitalSeminormedRing π•œ] (x y : closedBall (0 : π•œ) 1) :
70-
↑(x * y) = (x * y : π•œ) :=
110+
protected theorem Metric.unitClosedBall.coe_mul [NonUnitalSeminormedRing π•œ]
111+
(x y : closedBall (0 : π•œ) 1) : ↑(x * y) = (x * y : π•œ) :=
71112
rfl
72113

114+
@[deprecated (since := "2025-04-18")]
115+
alias coe_mul_unitClosedBall := Metric.unitClosedBall.coe_mul
116+
117+
instance Metric.unitClosedBall.instZero [Zero π•œ] [PseudoMetricSpace π•œ] :
118+
Zero (closedBall (0 : π•œ) 1) where
119+
zero := ⟨0, by simp⟩
120+
121+
@[simp, norm_cast]
122+
protected lemma Metric.unitClosedBall.coe_zero [Zero π•œ] [PseudoMetricSpace π•œ] :
123+
((0 : closedBall (0 : π•œ) 1) : π•œ) = 0 :=
124+
rfl
125+
126+
@[simp, norm_cast]
127+
protected lemma Metric.unitClosedBall.coe_eq_zero [Zero π•œ] [PseudoMetricSpace π•œ]
128+
{a : closedBall (0 : π•œ) 1} : (a : π•œ) = 0 ↔ a = 0 :=
129+
Subtype.val_injective.eq_iff' unitClosedBall.coe_zero
130+
131+
instance Metric.unitClosedBall.instSemigroupWithZero [NonUnitalSeminormedRing π•œ] :
132+
SemigroupWithZero (closedBall (0 : π•œ) 1) where
133+
zero_mul _ := Subtype.eq <| zero_mul _
134+
mul_zero _ := Subtype.eq <| mul_zero _
135+
73136
/-- Closed unit ball in a seminormed ring as a bundled `Submonoid`. -/
74137
def Submonoid.unitClosedBall (π•œ : Type*) [SeminormedRing π•œ] [NormOneClass π•œ] : Submonoid π•œ :=
75138
{ Subsemigroup.unitClosedBall π•œ with
76139
carrier := closedBall 0 1
77140
one_mem' := mem_closedBall_zero_iff.2 norm_one.le }
78141

79-
instance Metric.unitClosedBall.monoid [SeminormedRing π•œ] [NormOneClass π•œ] :
142+
instance Metric.unitClosedBall.instMonoid [SeminormedRing π•œ] [NormOneClass π•œ] :
80143
Monoid (closedBall (0 : π•œ) 1) :=
81144
SubmonoidClass.toMonoid (Submonoid.unitClosedBall π•œ)
82145

83-
instance Metric.unitClosedBall.commMonoid [SeminormedCommRing π•œ] [NormOneClass π•œ] :
146+
instance Metric.unitClosedBall.instCommMonoid [SeminormedCommRing π•œ] [NormOneClass π•œ] :
84147
CommMonoid (closedBall (0 : π•œ) 1) :=
85148
SubmonoidClass.toCommMonoid (Submonoid.unitClosedBall π•œ)
86149

87150
@[simp, norm_cast]
88-
theorem coe_one_unitClosedBall [SeminormedRing π•œ] [NormOneClass π•œ] :
151+
protected theorem Metric.unitClosedBall.coe_one [SeminormedRing π•œ] [NormOneClass π•œ] :
89152
((1 : closedBall (0 : π•œ) 1) : π•œ) = 1 :=
90153
rfl
91154

155+
@[deprecated (since := "2025-04-18")]
156+
alias coe_one_unitClosedBall := Metric.unitClosedBall.coe_one
157+
92158
@[simp, norm_cast]
93-
theorem coe_pow_unitClosedBall [SeminormedRing π•œ] [NormOneClass π•œ] (x : closedBall (0 : π•œ) 1)
94-
(n : β„•) : ↑(x ^ n) = (x : π•œ) ^ n :=
159+
protected theorem Metric.unitClosedBall.coe_eq_one [SeminormedRing π•œ] [NormOneClass π•œ]
160+
{a : closedBall (0 : π•œ) 1} : (a : π•œ) = 1 ↔ a = 1 :=
161+
Subtype.val_injective.eq_iff' unitClosedBall.coe_one
162+
163+
@[simp, norm_cast]
164+
protected theorem Metric.unitClosedBall.coe_pow [SeminormedRing π•œ] [NormOneClass π•œ]
165+
(x : closedBall (0 : π•œ) 1) (n : β„•) : ↑(x ^ n) = (x : π•œ) ^ n :=
95166
rfl
96167

168+
@[deprecated (since := "2025-04-18")]
169+
alias coe_pow_unitClosedBall := Metric.unitClosedBall.coe_pow
170+
171+
instance Metric.unitClosedBall.instMonoidWithZero [SeminormedRing π•œ] [NormOneClass π•œ] :
172+
MonoidWithZero (closedBall (0 : π•œ) 1) where
173+
174+
instance Metric.unitClosedBall.instCancelMonoidWithZero [SeminormedRing π•œ] [IsCancelMulZero π•œ]
175+
[NormOneClass π•œ] : CancelMonoidWithZero (closedBall (0 : π•œ) 1) where
176+
toIsCancelMulZero := Subtype.val_injective.isCancelMulZero _ rfl fun _ _ ↦ rfl
177+
178+
/-!
179+
### Algebraic instances on the unit sphere
180+
-/
181+
97182
/-- Unit sphere in a seminormed ring (with strictly multiplicative norm) as a bundled
98183
`Submonoid`. -/
99184
@[simps]
@@ -105,63 +190,74 @@ def Submonoid.unitSphere (π•œ : Type*) [SeminormedRing π•œ] [NormMulClass π•œ
105190
simp [*]
106191
one_mem' := mem_sphere_zero_iff_norm.2 norm_one
107192

108-
instance Metric.unitSphere.inv [NormedDivisionRing π•œ] : Inv (sphere (0 : π•œ) 1) :=
109-
⟨fun x =>
110-
⟨x⁻¹,
111-
mem_sphere_zero_iff_norm.2 <| by
112-
rw [norm_inv, mem_sphere_zero_iff_norm.1 x.coe_prop, inv_one]⟩⟩
193+
instance Metric.unitSphere.instInv [NormedDivisionRing π•œ] : Inv (sphere (0 : π•œ) 1) where
194+
inv x := ⟨x⁻¹, mem_sphere_zero_iff_norm.2 <| by
195+
rw [norm_inv, mem_sphere_zero_iff_norm.1 x.coe_prop, inv_one]⟩
113196

114197
@[simp, norm_cast]
115-
theorem coe_inv_unitSphere [NormedDivisionRing π•œ] (x : sphere (0 : π•œ) 1) : ↑x⁻¹ = (x⁻¹ : π•œ) :=
198+
theorem Metric.unitSphere.coe_inv [NormedDivisionRing π•œ] (x : sphere (0 : π•œ) 1) :
199+
↑x⁻¹ = (x⁻¹ : π•œ) :=
116200
rfl
117201

118-
instance Metric.unitSphere.div [NormedDivisionRing π•œ] : Div (sphere (0 : π•œ) 1) :=
119-
⟨fun x y =>
120-
⟨x / y,
121-
mem_sphere_zero_iff_norm.2 <| by
122-
rw [norm_div, mem_sphere_zero_iff_norm.1 x.coe_prop, mem_sphere_zero_iff_norm.1 y.coe_prop,
123-
div_one]⟩⟩
202+
@[deprecated (since := "2025-04-18")]
203+
alias coe_inv_unitSphere := Metric.unitSphere.coe_inv
204+
205+
instance Metric.unitSphere.instDiv [NormedDivisionRing π•œ] : Div (sphere (0 : π•œ) 1) where
206+
div x y := .mk (x / y) <| mem_sphere_zero_iff_norm.2 <| by
207+
rw [norm_div, mem_sphere_zero_iff_norm.1 x.2, mem_sphere_zero_iff_norm.1 y.coe_prop, div_one]
124208

125209
@[simp, norm_cast]
126-
theorem coe_div_unitSphere [NormedDivisionRing π•œ] (x y : sphere (0 : π•œ) 1) :
210+
protected theorem Metric.unitSphere.coe_div [NormedDivisionRing π•œ] (x y : sphere (0 : π•œ) 1) :
127211
↑(x / y) = (x / y : π•œ) :=
128212
rfl
129213

130-
instance Metric.unitSphere.pow [NormedDivisionRing π•œ] : Pow (sphere (0 : π•œ) 1) β„€ :=
131-
⟨fun x n =>
132-
⟨(x : π•œ) ^ n, by
133-
rw [mem_sphere_zero_iff_norm, norm_zpow, mem_sphere_zero_iff_norm.1 x.coe_prop, one_zpow]⟩⟩
214+
@[deprecated (since := "2025-04-18")]
215+
alias coe_div_unitSphere := Metric.unitSphere.coe_div
216+
217+
instance Metric.unitSphere.instZPow [NormedDivisionRing π•œ] : Pow (sphere (0 : π•œ) 1) β„€ where
218+
pow x n := .mk ((x : π•œ) ^ n) <| by
219+
rw [mem_sphere_zero_iff_norm, norm_zpow, mem_sphere_zero_iff_norm.1 x.coe_prop, one_zpow]
134220

135221
@[simp, norm_cast]
136-
theorem coe_zpow_unitSphere [NormedDivisionRing π•œ] (x : sphere (0 : π•œ) 1) (n : β„€) :
222+
theorem Metric.unitSphere.coe_zpow [NormedDivisionRing π•œ] (x : sphere (0 : π•œ) 1) (n : β„€) :
137223
↑(x ^ n) = (x : π•œ) ^ n :=
138224
rfl
139225

140-
instance Metric.unitSphere.monoid [SeminormedRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ] :
226+
@[deprecated (since := "2025-04-18")]
227+
alias coe_zpow_unitSphere := Metric.unitSphere.coe_zpow
228+
229+
instance Metric.unitSphere.instMonoid [SeminormedRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ] :
141230
Monoid (sphere (0 : π•œ) 1) :=
142231
SubmonoidClass.toMonoid (Submonoid.unitSphere π•œ)
143232

144-
instance Metric.unitSphere.commMonoid [SeminormedCommRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ] :
233+
instance Metric.unitSphere.instCommMonoid [SeminormedCommRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ] :
145234
CommMonoid (sphere (0 : π•œ) 1) :=
146235
SubmonoidClass.toCommMonoid (Submonoid.unitSphere π•œ)
147236

148237
@[simp, norm_cast]
149-
theorem coe_one_unitSphere [SeminormedRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ] :
238+
protected theorem Metric.unitSphere.coe_one [SeminormedRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ] :
150239
((1 : sphere (0 : π•œ) 1) : π•œ) = 1 :=
151240
rfl
152241

242+
@[deprecated (since := "2025-04-18")]
243+
alias coe_one_unitSphere := Metric.unitSphere.coe_one
244+
153245
@[simp, norm_cast]
154-
theorem coe_mul_unitSphere [SeminormedRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ]
155-
(x y : sphere (0 : π•œ) 1) :
156-
↑(x * y) = (x * y : π•œ) :=
246+
theorem Metric.unitSphere.coe_mul [SeminormedRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ]
247+
(x y : sphere (0 : π•œ) 1) : ↑(x * y) = (x * y : π•œ) :=
157248
rfl
158249

250+
@[deprecated (since := "2025-04-18")]
251+
alias coe_mul_unitSphere := Metric.unitSphere.coe_mul
252+
159253
@[simp, norm_cast]
160-
theorem coe_pow_unitSphere [SeminormedRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ]
161-
(x : sphere (0 : π•œ) 1) (n : β„•) :
162-
↑(x ^ n) = (x : π•œ) ^ n :=
254+
theorem Metric.unitSphere.coe_pow [SeminormedRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ]
255+
(x : sphere (0 : π•œ) 1) (n : β„•) : ↑(x ^ n) = (x : π•œ) ^ n :=
163256
rfl
164257

258+
@[deprecated (since := "2025-04-18")]
259+
alias coe_pow_unitSphere := Metric.unitSphere.coe_pow
260+
165261
/-- Monoid homomorphism from the unit sphere in a normed division ring to the group of units. -/
166262
def unitSphereToUnits (π•œ : Type*) [NormedDivisionRing π•œ] : sphere (0 : π•œ) 1 β†’* Units π•œ :=
167263
Units.liftRight (Submonoid.unitSphere π•œ).subtype
@@ -176,25 +272,23 @@ theorem unitSphereToUnits_injective [NormedDivisionRing π•œ] :
176272
Function.Injective (unitSphereToUnits π•œ) := fun x y h =>
177273
Subtype.eq <| by convert congr_arg Units.val h
178274

179-
instance Metric.sphere.group [NormedDivisionRing π•œ] : Group (sphere (0 : π•œ) 1) :=
275+
instance Metric.unitSphere.instGroup [NormedDivisionRing π•œ] : Group (sphere (0 : π•œ) 1) :=
180276
unitSphereToUnits_injective.group (unitSphereToUnits π•œ) (Units.ext rfl)
181277
(fun _x _y => Units.ext rfl)
182278
(fun _x => Units.ext rfl) (fun _x _y => Units.ext <| div_eq_mul_inv _ _)
183279
(fun x n => Units.ext (Units.val_pow_eq_pow_val (unitSphereToUnits π•œ x) n).symm) fun x n =>
184280
Units.ext (Units.val_zpow_eq_zpow_val (unitSphereToUnits π•œ x) n).symm
185281

186-
instance Metric.sphere.hasDistribNeg [SeminormedRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ] :
282+
instance Metric.sphere.instHasDistribNeg [SeminormedRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ] :
187283
HasDistribNeg (sphere (0 : π•œ) 1) :=
188284
Subtype.coe_injective.hasDistribNeg ((↑) : sphere (0 : π•œ) 1 β†’ π•œ) (fun _ => rfl) fun _ _ => rfl
189285

190-
instance Metric.sphere.continuousMul [SeminormedRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ] :
286+
instance Metric.sphere.instContinuousMul [SeminormedRing π•œ] [NormMulClass π•œ] [NormOneClass π•œ] :
191287
ContinuousMul (sphere (0 : π•œ) 1) :=
192288
(Submonoid.unitSphere π•œ).continuousMul
193289

194-
instance Metric.sphere.topologicalGroup [NormedDivisionRing π•œ] :
290+
instance Metric.sphere.instIsTopologicalGroup [NormedDivisionRing π•œ] :
195291
IsTopologicalGroup (sphere (0 : π•œ) 1) where
196292
continuous_inv := (continuous_subtype_val.invβ‚€ ne_zero_of_mem_unit_sphere).subtype_mk _
197293

198-
instance Metric.sphere.commGroup [NormedField π•œ] : CommGroup (sphere (0 : π•œ) 1) :=
199-
{ Metric.sphere.group,
200-
Subtype.coe_injective.commMonoid _ rfl (fun _ _ => rfl) (fun _ _ => rfl) with }
294+
instance Metric.sphere.instCommGroup [NormedField π•œ] : CommGroup (sphere (0 : π•œ) 1) where

0 commit comments

Comments
Β (0)