@@ -17,120 +17,121 @@ assert_not_exists Set.range Monoid DenselyOrdered
1717
1818open Function
1919
20- universe u v₁ v₂ v₃
21-
22- variable {I : Type u}
23-
24- -- The indexing type
25- variable {α β γ : Type *}
26-
27- -- The families of types already equipped with instances
28- variable {f : I → Type v₁} (x y : ∀ i, f i) (i : I)
20+ variable {ι α β : Type *} {G M : ι → Type *}
2921
3022namespace Pi
3123
3224/-! `1`, `0`, `+`, `*`, `+ᵥ`, `•`, `^`, `-`, `⁻¹`, and `/` are defined pointwise. -/
3325
26+ section One
27+ variable [∀ i, One (M i)]
28+
3429@[to_additive]
35- instance instOne [∀ i, One <| f i] : One (∀ i : I, f i) :=
36- ⟨fun _ => 1 ⟩
30+ instance instOne : One (∀ i, M i) where one _ := 1
3731
3832@[to_additive (attr := simp high)]
39- theorem one_apply [∀ i, One <| f i] : (1 : ∀ i, f i) i = 1 :=
40- rfl
33+ lemma one_apply (i : ι) : (1 : ∀ i, M i) i = 1 := rfl
4134
4235@[to_additive]
43- theorem one_def [∀ i, One <| f i] : (1 : ∀ i, f i) = fun _ => 1 :=
44- rfl
36+ lemma one_def : (1 : ∀ i, M i) = fun _ ↦ 1 := rfl
4537
46- @[to_additive (attr := simp)] lemma _root_.Function.const_one [One β] : const α ( 1 : β) = 1 := rfl
38+ variable {M : Type *} [One M]
4739
48- @[to_additive (attr := simp)]
49- theorem one_comp [One γ] (x : α → β) : (1 : β → γ) ∘ x = 1 :=
50- rfl
40+ @[to_additive (attr := simp)] lemma _root_.Function.const_one : const α (1 : M) = 1 := rfl
5141
52- @[to_additive (attr := simp)]
53- theorem comp_one [One β] (x : β → γ) : x ∘ (1 : α → β) = const α (x 1 ) :=
54- rfl
42+ @[to_additive (attr := simp)] lemma one_comp (f : α → β) : (1 : β → M) ∘ f = 1 := rfl
43+ @[to_additive (attr := simp)] lemma comp_one (f : M → β) : f ∘ (1 : α → M) = const α (f 1 ) := rfl
5544
56- @[to_additive]
57- instance instMul [∀ i, Mul <| f i] : Mul (∀ i : I, f i) :=
58- ⟨fun f g i => f i * g i⟩
45+ end One
5946
60- @[to_additive (attr := simp)]
61- theorem mul_apply [∀ i, Mul <| f i] : (x * y) i = x i * y i :=
62- rfl
47+ section Mul
48+ variable [∀ i, Mul (M i)]
6349
6450@[to_additive]
65- theorem mul_def [∀ i, Mul <| f i] : x * y = fun i => x i * y i :=
66- rfl
51+ instance instMul : Mul (∀ i, M i) where mul f g i := f i * g i
6752
6853@[to_additive (attr := simp)]
69- lemma _root_.Function.const_mul [Mul β] (a b : β) : const α a * const α b = const α (a * b) := rfl
70-
71- @[to_additive]
72- theorem mul_comp [Mul γ] (x y : β → γ) (z : α → β) : (x * y) ∘ z = x ∘ z * y ∘ z :=
73- rfl
54+ lemma mul_apply (f g : ∀ i, M i) (i : ι) : (f * g) i = f i * g i := rfl
7455
7556@[to_additive]
76- instance instSMul [∀ i, SMul α <| f i] : SMul α (∀ i : I, f i) :=
77- ⟨fun s x => fun i => s • x i⟩
57+ lemma mul_def (f g : ∀ i, M i) : f * g = fun i ↦ f i * g i := rfl
7858
79- @[to_additive existing instSMul]
80- instance instPow [∀ i, Pow (f i) β] : Pow (∀ i, f i) β :=
81- ⟨fun x b i => x i ^ b⟩
59+ variable {M : Type *} [Mul M]
8260
83- @[to_additive (attr := simp, to_additive) (reorder := 5 6) smul_apply]
84- theorem pow_apply [∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) (i : I) : (x ^ b) i = x i ^ b :=
85- rfl
61+ @[to_additive (attr := simp)]
62+ lemma _root_.Function.const_mul (a b : M) : const ι a * const ι b = const ι (a * b) := rfl
8663
87- @[to_additive (attr := to_additive) (reorder := 5 6) smul_def]
88- theorem pow_def [∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) : x ^ b = fun i => x i ^ b :=
89- rfl
64+ @[to_additive]
65+ lemma mul_comp (f g : β → M) (z : α → β) : (f * g) ∘ z = f ∘ z * g ∘ z := rfl
9066
91- @[to_additive (attr := simp, to_additive) (reorder := 2 3, 5 6) smul_const]
92- lemma _root_.Function.const_pow [Pow α β] (a : α) (b : β) : const I a ^ b = const I (a ^ b) := rfl
67+ end Mul
9368
94- @[to_additive (attr := to_additive) (reorder := 6 7) smul_comp]
95- theorem pow_comp [Pow γ α] (x : β → γ) (a : α) (y : I → β) : (x ^ a) ∘ y = x ∘ y ^ a :=
96- rfl
69+ section Inv
70+ variable [∀ i, Inv (G i)]
9771
9872@[to_additive]
99- instance instInv [∀ i, Inv <| f i] : Inv (∀ i : I, f i) :=
100- ⟨fun f i => (f i)⁻¹⟩
73+ instance instInv : Inv (∀ i, G i) where inv f i := (f i)⁻¹
10174
10275@[to_additive (attr := simp)]
103- theorem inv_apply [∀ i, Inv <| f i] : x⁻¹ i = (x i)⁻¹ :=
104- rfl
76+ lemma inv_apply (f : ∀ i, G i) (i : ι) : f⁻¹ i = (f i)⁻¹ := rfl
10577
10678@[to_additive]
107- theorem inv_def [∀ i, Inv <| f i] : x⁻¹ = fun i => (x i)⁻¹ :=
108- rfl
79+ lemma inv_def (f : ∀ i, G i) : f⁻¹ = fun i ↦ (f i)⁻¹ := rfl
80+
81+ variable {G : Type *} [Inv G]
10982
11083@[to_additive]
111- lemma _root_.Function.const_inv [Inv β] (a : β ) : (const α a)⁻¹ = const α a⁻¹ := rfl
84+ lemma _root_.Function.const_inv (a : G ) : (const ι a)⁻¹ = const ι a⁻¹ := rfl
11285
11386@[to_additive]
114- theorem inv_comp [Inv γ] (x : β → γ) (y : α → β) : x⁻¹ ∘ y = (x ∘ y)⁻¹ :=
115- rfl
87+ lemma inv_comp (f : β → G) (g : α → β) : f⁻¹ ∘ g = (f ∘ g)⁻¹ := rfl
88+ end Inv
89+
90+ section Div
91+ variable [∀ i, Div (G i)]
11692
11793@[to_additive]
118- instance instDiv [∀ i, Div <| f i] : Div (∀ i : I, f i) :=
119- ⟨fun f g i => f i / g i⟩
94+ instance instDiv : Div (∀ i, G i) where div f g i := f i / g i
12095
12196@[to_additive (attr := simp)]
122- theorem div_apply [∀ i, Div <| f i] : (x / y) i = x i / y i :=
123- rfl
97+ lemma div_apply (f g : ∀ i, G i) (i : ι) : (f / g) i = f i / g i :=rfl
12498
12599@[to_additive]
126- theorem div_def [∀ i, Div <| f i] : x / y = fun i => x i / y i :=
127- rfl
100+ lemma div_def (f g : ∀ i, G i) : f / g = fun i ↦ f i / g i := rfl
101+
102+ variable {G : Type *} [Div G]
128103
129104@[to_additive]
130- theorem div_comp [Div γ] (x y : β → γ) (z : α → β) : (x / y) ∘ z = x ∘ z / y ∘ z :=
131- rfl
105+ lemma div_comp (f g : β → G) (z : α → β) : (f / g) ∘ z = f ∘ z / g ∘ z := rfl
132106
133107@[to_additive (attr := simp)]
134- lemma _root_.Function.const_div [Div β] (a b : β) : const α a / const α b = const α (a / b) := rfl
108+ lemma _root_.Function.const_div (a b : G) : const ι a / const ι b = const ι (a / b) := rfl
109+
110+ end Div
111+
112+ section Pow
113+
114+ @[to_additive]
115+ instance instSMul [∀ i, SMul α (M i)] : SMul α (∀ i, M i) where smul a f i := a • f i
116+
117+ variable [∀ i, Pow (M i) α]
118+
119+ @[to_additive existing instSMul]
120+ instance instPow : Pow (∀ i, M i) α where pow f a i := f i ^ a
121+
122+ @[to_additive (attr := simp, to_additive) (reorder := 5 6) smul_apply]
123+ lemma pow_apply (f : ∀ i, M i) (a : α) (i : ι) : (f ^ a) i = f i ^ a := rfl
124+
125+ @[to_additive (attr := to_additive) (reorder := 5 6) smul_def]
126+ lemma pow_def (f : ∀ i, M i) (a : α) : f ^ a = fun i ↦ f i ^ a := rfl
127+
128+ variable {M : Type *} [Pow M α]
129+
130+ @[to_additive (attr := simp, to_additive) (reorder := 2 3, 5 6) smul_const]
131+ lemma _root_.Function.const_pow (a : M) (b : α) : const ι a ^ b = const ι (a ^ b) := rfl
132+
133+ @[to_additive (attr := to_additive) (reorder := 6 7) smul_comp]
134+ lemma pow_comp (f : β → M) (a : α) (g : ι → β) : (f ^ a) ∘ g = f ∘ g ^ a := rfl
135135
136+ end Pow
136137end Pi
0 commit comments