feat(data/{pi, prod}): add missing has_pow instances for pi type (#…

…15478)

This generalizes the existing powers by `nat` and `int` defined in later files to be defined for arbitrary powers.
As well as eliminating the need for separate lemmas for these different power operations, this also means that tuples of real numbers now inherit a power operation by the real numbers.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/group/pi.lean

@@ -43,10 +43,6 @@ instance monoid [∀ i, monoid $ f i] : monoid (Π i : I, f i) :=
 by refine_struct { one := (1 : Π i, f i), mul := (*), npow := λ n x i, (x i) ^ n };
 tactic.pi_instance_derive_field
 
--- the attributes are intentionally out of order. `smul_apply` proves `nsmul_apply`.
-@[to_additive, simp]
-lemma pow_apply [∀ i, monoid $ f i] (n : ℕ) : (x^n) i = (x i)^n := rfl
-
 @[to_additive]
 instance comm_monoid [∀ i, comm_monoid $ f i] : comm_monoid (Π i : I, f i) :=
 by refine_struct { one := (1 : Π i, f i), mul := (*), npow := monoid.npow };

src/data/pi/algebra.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Eric Wieser
 -/
 import algebra.group.to_additive
+import algebra.group.defs
 import data.prod.basic
 import logic.unique
 import tactic.congr
@@ -30,7 +31,7 @@ variables (x y : Π i, f i) (i : I)
 
 namespace pi
 
-/-! `1`, `0`, `+`, `*`, `-`, `⁻¹`, and `/` are defined pointwise. -/
+/-! `1`, `0`, `+`, `*`, `+ᵥ`, `•`, `^`, `-`, `⁻¹`, and `/` are defined pointwise. -/
 
 @[to_additive] instance has_one [∀ i, has_one $ f i] :
   has_one (Π i : I, f i) :=
@@ -59,6 +60,38 @@ instance has_mul [∀ i, has_mul $ f i] :
 @[to_additive] lemma mul_comp [has_mul γ] (x y : β → γ) (z : α → β) :
   (x * y) ∘ z = x ∘ z * y ∘ z := rfl
 
+@[to_additive pi.has_vadd] instance has_smul [Π i, has_smul α $ f i] : has_smul α (Π i : I, f i) :=
+⟨λ s x, λ i, s • (x i)⟩
+
+@[simp, to_additive] lemma smul_apply [Π i, has_smul α $ f i] (s : α) (x : Π i, f i) (i : I) :
+  (s • x) i = s • x i := rfl
+
+@[to_additive] lemma smul_def [Π i, has_smul α $ f i] (s : α) (x : Π i, f i) :
+  s • x = λ i, s • x i := rfl
+
+@[simp, to_additive]
+lemma smul_const [has_smul α β] (a : α) (b : β) : a • const I b = const I (a • b) := rfl
+
+@[to_additive]
+lemma smul_comp [has_smul α γ] (a : α) (x : β → γ) (y : I → β) : (a • x) ∘ y = a • (x ∘ y) := rfl
+
+@[to_additive pi.has_smul]
+instance has_pow [Π i, has_pow (f i) β] : has_pow (Π i, f i) β :=
+⟨λ x b i, (x i) ^ b⟩
+
+@[simp, to_additive pi.smul_apply, to_additive_reorder 5]
+lemma pow_apply [Π i, has_pow (f i) β] (x : Π i, f i) (b : β) (i : I) : (x ^ b) i = (x i) ^ b := rfl
+
+@[to_additive pi.smul_def, to_additive_reorder 5]
+lemma pow_def [Π i, has_pow (f i) β] (x : Π i, f i) (b : β) : x ^ b = λ i, (x i) ^ b := rfl
+
+-- `to_additive` generates bad output if we take `has_pow α β`.
+@[simp, to_additive smul_const, to_additive_reorder 5]
+lemma const_pow [has_pow β α] (b : β) (a : α) : const I b ^ a = const I (b ^ a) := rfl
+
+@[to_additive smul_comp, to_additive_reorder 6]
+lemma pow_comp [has_pow γ α] (x : β → γ) (a : α) (y : I → β) : (x ^ a) ∘ y = (x ∘ y) ^ a := rfl
+
 @[simp] lemma bit0_apply [Π i, has_add $ f i] : (bit0 x) i = bit0 (x i) := rfl
 
 @[simp] lemma bit1_apply [Π i, has_add $ f i] [Π i, has_one $ f i] : (bit1 x) i = bit1 (x i) := rfl

src/group_theory/group_action/pi.lean

@@ -26,16 +26,6 @@ variables (x y : Π i, f i) (i : I)
 
 namespace pi
 
-@[to_additive pi.has_vadd]
-instance has_smul {α : Type*} [Π i, has_smul α $ f i] :
-  has_smul α (Π i : I, f i) :=
-⟨λ s x, λ i, s • (x i)⟩
-
-@[to_additive]
-lemma smul_def {α : Type*} [Π i, has_smul α $ f i] (s : α) : s • x = λ i, s • x i := rfl
-@[simp, to_additive]
-lemma smul_apply {α : Type*} [Π i, has_smul α $ f i] (s : α) : (s • x) i = s • x i := rfl
-
 @[to_additive pi.has_vadd']
 instance has_smul' {g : I → Type*} [Π i, has_smul (f i) (g i)] :
   has_smul (Π i, f i) (Π i : I, g i) :=

src/group_theory/group_action/prod.lean

@@ -25,7 +25,7 @@ scalar multiplication as a homomorphism from `α × β` to `β`.
 * `group_theory.group_action.sum`
 -/
 
-variables {M N P α β : Type*}
+variables {M N P E α β : Type*}
 
 namespace prod
 
@@ -41,6 +41,24 @@ variables [has_smul M α] [has_smul M β] [has_smul N α] [has_smul N β] (a : M
 @[to_additive] theorem smul_def (a : M) (x : α × β) : a • x = (a • x.1, a • x.2) := rfl
 @[simp, to_additive] theorem smul_swap : (a • x).swap = a • x.swap := rfl
 
+
+variables [has_pow α E] [has_pow β E]
+@[to_additive has_smul] instance has_pow : has_pow (α × β) E :=
+{ pow := λ p c, (p.1 ^ c, p.2 ^ c) }
+@[simp, to_additive smul_snd, to_additive_reorder 6]
+lemma pow_fst (p : α × β) (c : E) : (p ^ c).fst = p.fst ^ c := rfl
+@[simp, to_additive smul_snd, to_additive_reorder 6]
+lemma pow_snd (p : α × β) (c : E) : (p ^ c).snd = p.snd ^ c := rfl
+/- Note that the `c` arguments to this lemmas cannot be in the more natural right-most positions due
+to limitations in `to_additive` and `to_additive_reorder`, which will silently fail to reorder more
+than two adjacent arguments -/
+@[simp, to_additive smul_mk, to_additive_reorder 6]
+lemma pow_mk (c : E) (a : α) (b : β) : (prod.mk a b) ^ c = prod.mk (a ^ c) (b ^ c) := rfl
+@[to_additive smul_def, to_additive_reorder 6]
+lemma pow_def (p : α × β) (c : E) : p ^ c = (p.1 ^ c, p.2 ^ c) := rfl
+@[simp, to_additive smul_swap, to_additive_reorder 6]
+lemma pow_swap (p : α × β) (c : E) : (p ^ c).swap = p.swap ^ c := rfl
+
 instance [has_smul M N] [is_scalar_tower M N α] [is_scalar_tower M N β] :
   is_scalar_tower M N (α × β) :=
 ⟨λ x y z, mk.inj_iff.mpr ⟨smul_assoc _ _ _, smul_assoc _ _ _⟩⟩

src/topology/continuous_function/polynomial.lean

@@ -61,7 +61,7 @@ variables {α : Type*} [topological_space α]
 begin
   apply polynomial.induction_on' g,
   { intros p q hp hq, simp [hp, hq], },
-  { intros n a, simp [pi.pow_apply f x n], },
+  { intros n a, simp [pi.pow_apply], },
 end
 
 end