drop IndexType namespace on sum and product

SciLean/Algebra/IsAddGroupHom.lean

@@ -128,11 +128,11 @@ theorem HSub.hSub.arg_a0a1.IsAddGroupHom_rule
   · simp [hf.map_neg,hg.map_neg,add_comm,←neg_add_eq_sub]
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.IsAddGroupHom_rule
+theorem sum.arg_f.IsAddGroupHom_rule
   [IndexType ι]
   (f : X → ι → Y) (hf : ∀ i, IsAddGroupHom (f · i))
   : IsAddGroupHom fun x => ∑ i, f x i := by have := hf; sorry_proof

SciLean/Algebra/IsAffineMap.lean

@@ -172,11 +172,11 @@ theorem HMul.hMul.arg_a1.IsAffineMap_rule
   (f : X → R) (hf : IsAffineMap R f) (y' : R) : IsAffineMap 𝕜 fun x => y' * f x := sorry_proof
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.IsAffineMap_rule
+theorem sum.arg_f.IsAffineMap_rule
   (f : X → ι → Y) (hf : ∀ i, IsAffineMap R (f · i))
   : IsAffineMap R fun x => ∑ i, f x i := by sorry_proof
 

SciLean/Algebra/IsLinearMap.lean

@@ -266,11 +266,11 @@ theorem HSMul.hSMul.arg_a1.IsLinearMap_rule_int
   intro x y; simp[hf.1]
   intro c x; simp[hf.2]; rw [@smul_comm]
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.IsLinearMap_rule
+theorem sum.arg_f.IsLinearMap_rule
   (f : X → ι → Y) (hf : ∀ i, IsLinearMap R (f · i))
   : IsLinearMap R fun x => ∑ i, f x i := by sorry_proof
 

SciLean/Analysis/AdjointSpace/Adjoint.lean

@@ -210,7 +210,7 @@ theorem pi_rule
     (f : X → (i : ι) → E i) (hf : ∀ i, IsContinuousLinearMap K (f · i)) :
     (fun (x : X) (i : ι) => f x i)†
     =
-    (fun x' => IndexType.sum fun i => ((f · i)†) (x' i)) := by
+    (fun x' => sum fun i => ((f · i)†) (x' i)) := by
 
   rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
   intro x y
@@ -406,11 +406,11 @@ by
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.adjoint_rule {ι} [IndexType ι]
+theorem sum.arg_f.adjoint_rule {ι} [IndexType ι]
   (f : X → ι → Y) (hf : ∀ i, IsContinuousLinearMap K (f · i))
-  : (fun x => IndexType.sum fun i => f x i)†
+  : (fun x => sum fun i => f x i)†
     =
-    (fun y => IndexType.sum fun i => ((f · i)†) y) :=
+    (fun y => sum fun i => ((f · i)†) y) :=
 by
   rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
   sorry_proof

SciLean/Analysis/AdjointSpace/AdjointProj.lean

@@ -643,7 +643,7 @@ def HPow.hPow.arg_a0.adjointProjUpdate_rule
   unfold adjointProjUpdate; fun_trans
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 section IndexTypeSum
@@ -652,7 +652,7 @@ variable {ι : Type} [IndexType ι]
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.adjointProj_rule [DecidableEq ι]
+theorem sum.arg_f.adjointProj_rule [DecidableEq ι]
     (f : X → ι → Y') (hf : ∀ i, IsContinuousLinearMap K (fun x => f x i)) :
     adjointProj K Yi (fun x => ∑ i, f x i)
     =
@@ -670,7 +670,7 @@ theorem IndexType.sum.arg_f.adjointProj_rule [DecidableEq ι]
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.adjointProjUpdate_rule [DecidableEq ι]
+theorem sum.arg_f.adjointProjUpdate_rule [DecidableEq ι]
     (f : X → ι → Y') (hf : ∀ i, IsContinuousLinearMap K (fun x => f x i)) :
     adjointProjUpdate K Yi (fun x => ∑ i, f x i)
     =

SciLean/Analysis/AdjointSpace/Basic.lean

@@ -305,8 +305,8 @@ instance : AdjointSpace 𝕜 ((i : ι) → E i) where
     -- apply Exists.intro (∑ i, d i ^ 2)
     sorry_proof
   conj_symm := by simp; sorry_proof
-  add_left := by simp[inner_add_left,SciLean.IndexType.sum_add_distrib]
-  smul_left := by simp[inner_smul_left,SciLean.IndexType.mul_sum]
+  add_left := by simp[inner_add_left,SciLean.sum_add_distrib]
+  smul_left := by simp[inner_smul_left,SciLean.mul_sum]
 
 
 theorem inner_prod_split (x y : X×Y) : ⟪x,y⟫_𝕜 = ⟪x.1,y.1⟫_𝕜 + ⟪x.2,y.2⟫_𝕜 := by rfl

SciLean/Analysis/Calculus/CDeriv.lean

@@ -450,11 +450,11 @@ def HPow.hPow.arg_a0.cderiv_rule (n : Nat)
   funext x; fun_trans
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.cderiv_rule_at
+theorem sum.arg_f.cderiv_rule_at
   (f : X → ι → Y) (x : X) (hf : ∀ i, CDifferentiableAt K (f · i) x)
   : cderiv K (fun x => ∑ i, f x i) x
     =
@@ -465,7 +465,7 @@ by
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.cderiv_rule
+theorem sum.arg_f.cderiv_rule
   (f : X → ι → Y) (hf : ∀ i, CDifferentiable K (f · i))
   : cderiv K (fun x => ∑ i, f x i)
     =

SciLean/Analysis/Calculus/FDeriv.lean

@@ -390,12 +390,12 @@ by
 --------------------------------------------------------------------------------
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.fderiv_rule_at {ι} [IndexType ι]
+theorem sum.arg_f.fderiv_rule_at {ι} [IndexType ι]
   (x : X) (f : X → ι → Y) (hf : ∀ i, DifferentiableAt K (f · i) x)
-  : fderiv K (fun x => IndexType.sum fun i => f x i) x
+  : fderiv K (fun x => sum fun i => f x i) x
     =
     fun dx =>L[K]
-      IndexType.sum fun i =>
+      sum fun i =>
         let dy := fderiv K (f · i) x dx
         dy :=
 by
@@ -405,12 +405,12 @@ by
   apply hf
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.fderiv_rule {ι} [IndexType ι]
+theorem sum.arg_f.fderiv_rule {ι} [IndexType ι]
   (f : X → ι → Y) (hf : ∀ i, Differentiable K (f · i))
-  : fderiv K (fun x => IndexType.sum fun i => f x i)
+  : fderiv K (fun x => sum fun i => f x i)
     =
     fun x => fun dx =>L[K]
-      IndexType.sum fun i =>
+      sum fun i =>
         let dy := fderiv K (f · i) x dx
         dy :=
 by

SciLean/Analysis/Calculus/FwdCDeriv.lean

@@ -364,11 +364,11 @@ def HPow.hPow.arg_a0.fwdCDeriv_rule (n : Nat)
   unfold fwdCDeriv; fun_trans
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.fwdCDeriv_rule_at (x : X)
+theorem sum.arg_f.fwdCDeriv_rule_at (x : X)
     (f : X → ι → Y) (hf : ∀ i, CDifferentiableAt K (f · i) x) :
     fwdCDeriv K (fun x => ∑ i, f x i) x
     =
@@ -378,7 +378,7 @@ theorem IndexType.sum.arg_f.fwdCDeriv_rule_at (x : X)
   unfold fwdCDeriv; fun_trans; sorry_proof -- need linearity of prod.mk
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.fwdCDeriv_rule
+theorem sum.arg_f.fwdCDeriv_rule
     (f : X → ι → Y) (hf : ∀ i, CDifferentiable K (f · i)) :
     fwdCDeriv K (fun x => ∑ i, f x i)
     =

SciLean/Analysis/Calculus/FwdFDeriv.lean

@@ -385,7 +385,7 @@ def HPow.hPow.arg_a0.fwdFDeriv_rule (n : Nat) :
   unfold fwdFDeriv; fun_trans
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 open BigOperators in
@@ -403,12 +403,12 @@ theorem FinType.sum.arg_f.fwdFDeriv_rule_at (x : X) (A : Finset ι)
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.fwdFDeriv_rule_at {ι} [IndexType ι]
+theorem sum.arg_f.fwdFDeriv_rule_at {ι} [IndexType ι]
   (x : X) (f : X → ι → Y) (hf : ∀ i, DifferentiableAt K (f · i) x)
-  : fwdFDeriv K (fun x => IndexType.sum fun i => f x i) x
+  : fwdFDeriv K (fun x => sum fun i => f x i) x
     =
     fun dx =>
-      IndexType.sum fun i =>
+      sum fun i =>
         let ydy := fwdFDeriv K (f · i) x dx
         ydy :=
 by
@@ -417,12 +417,12 @@ by
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.fwdFDeriv_rule {ι} [IndexType ι]
+theorem sum.arg_f.fwdFDeriv_rule {ι} [IndexType ι]
   (f : X → ι → Y) (hf : ∀ i, Differentiable K (f · i))
-  : fwdFDeriv K (fun x => IndexType.sum fun i => f x i)
+  : fwdFDeriv K (fun x => sum fun i => f x i)
     =
     fun x dx =>
-      IndexType.sum fun i =>
+      sum fun i =>
         let ydy := fwdFDeriv K (f · i) x dx
         ydy :=
 by

SciLean/Analysis/Calculus/RevCDeriv.lean

@@ -222,7 +222,7 @@ theorem pi_rule
   fun_trans;
   funext x; simp
   rw[cderiv.pi_rule (hf:=by fun_prop)]; fun_trans
-  simp[revCDerivUpdate,revCDeriv,IndexType.sum]
+  simp[revCDerivUpdate,revCDeriv,sum]
   sorry_proof
 
 end revCDeriv
@@ -1176,15 +1176,15 @@ def HPow.hPow.arg_a0.revCDerivProjUpdate_rule
   unfold revCDerivProjUpdate; fun_trans; simp[oneHot,structMake,revCDerivUpdate]
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 section IndexTypeSum
 
 variable {ι : Type} [IndexType ι]
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revCDeriv_rule
+theorem sum.arg_f.revCDeriv_rule
   (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (fun x => f x i))
   : revCDeriv K (fun x => ∑ i, f x i)
     =
@@ -1202,7 +1202,7 @@ by
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revCDerivUpdate_rule
+theorem sum.arg_f.revCDerivUpdate_rule
     (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (fun x => f x i)) :
     revCDerivUpdate K (fun x => ∑ i, f x i)
     =
@@ -1215,7 +1215,7 @@ theorem IndexType.sum.arg_f.revCDerivUpdate_rule
   fun_trans
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revCDerivProj_rule [DecidableEq ι]
+theorem sum.arg_f.revCDerivProj_rule [DecidableEq ι]
     (f : X → ι → Y') (hf : ∀ i, HasAdjDiff K (fun x => f x i)) :
     revCDerivProj K Yi (fun x => ∑ i, f x i)
     =
@@ -1233,7 +1233,7 @@ theorem IndexType.sum.arg_f.revCDerivProj_rule [DecidableEq ι]
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revCDerivProjUpdate_rule [DecidableEq ι]
+theorem sum.arg_f.revCDerivProjUpdate_rule [DecidableEq ι]
     (f : X → ι → Y') (hf : ∀ i, HasAdjDiff K (fun x => f x i)) :
     revCDerivProjUpdate K Yi (fun x => ∑ i, f x i)
     =

SciLean/Analysis/Calculus/RevFDeriv.lean

@@ -118,7 +118,7 @@ theorem pi_rule
     =
     fun x =>
       (fun i => f x i,
-       fun dy => IndexType.sum fun i =>
+       fun dy => sum fun i =>
          let dx := (revFDeriv K (f · i) x).2 (dy i)
          dx)
        := by
@@ -169,7 +169,7 @@ theorem pi_rule_at
     (revFDeriv K fun (x : X) (i : ι) => f x i) x
     =
     (fun i => f x i,
-     fun dy => IndexType.sum fun i =>
+     fun dy => sum fun i =>
        let dx := (revFDeriv K (f · i) x).2 (dy i)
        dx) := by
   unfold revFDeriv
@@ -504,13 +504,13 @@ def HPow.hPow.arg_a0.revFDeriv_rule
 --------------------------------------------------------------------------------
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revFDeriv_rule_at {ι} [IndexType ι]
+theorem sum.arg_f.revFDeriv_rule_at {ι} [IndexType ι]
   (x : X) (f : X → ι → Y) (hf : ∀ i, DifferentiableAt K (f · i) x)
-  : revFDeriv K (fun x => IndexType.sum fun i => f x i) x
+  : revFDeriv K (fun x => sum fun i => f x i) x
     =
-    (IndexType.sum fun i => f x i,
+    (sum fun i => f x i,
      fun dy =>
-       IndexType.sum fun i =>
+       sum fun i =>
          let dx := adjointFDeriv K (f · i) x dy
          dx) :=
 
@@ -520,13 +520,13 @@ by
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revFDeriv_rule {ι} [IndexType ι]
+theorem sum.arg_f.revFDeriv_rule {ι} [IndexType ι]
   (f : X → ι → Y) (hf : ∀ i, Differentiable K (f · i))
-  : revFDeriv K (fun x => IndexType.sum fun i => f x i)
+  : revFDeriv K (fun x => sum fun i => f x i)
     =
     fun x =>
-    (IndexType.sum fun i => f x i,
+    (sum fun i => f x i,
      fun dy =>
-       IndexType.sum fun i =>
+       sum fun i =>
          let dx := adjointFDeriv K (f · i) x dy
          dx) := by funext x; fun_trans

SciLean/Analysis/Calculus/RevFDerivProj.lean

@@ -837,14 +837,14 @@ def HPow.hPow.arg_a0.revFDerivProjUpdate_rule
   unfold revFDerivProjUpdate; fun_trans
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 section IndexTypeSum
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revFDerivProj_rule
+theorem sum.arg_f.revFDerivProj_rule
     (f : X → ι → Y') (hf : ∀ i, Differentiable K (fun x => f x i)) :
     revFDerivProj K Yi (fun x => ∑ i, f x i)
     =
@@ -859,7 +859,7 @@ theorem IndexType.sum.arg_f.revFDerivProj_rule
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revFDerivProjUpdate_rule
+theorem sum.arg_f.revFDerivProjUpdate_rule
     (f : X → ι → Y') (hf : ∀ i, Differentiable K (fun x => f x i)) :
     revFDerivProjUpdate K Yi (fun x => ∑ i, f x i)
     =

SciLean/Analysis/Convenient/CDifferentiable.lean

@@ -348,20 +348,20 @@ def HPow.hPow.arg_a0.CDifferentiableAt_rule
 
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 ---------------------------------------------------------------------------------
 
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.CDifferentiableAt_rule
+theorem sum.arg_f.CDifferentiableAt_rule
   (f : X → ι → Y) (x : X) (hf : ∀ i, CDifferentiableAt K (fun x => f x i) x)
   : CDifferentiableAt K (fun x => ∑ i, f x i) x :=
 by
   sorry_proof
 
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.CDifferentiable_rule
+theorem sum.arg_f.CDifferentiable_rule
   (f : X → ι → Y) (hf : ∀ i, CDifferentiable K (fun x => f x i))
   : CDifferentiable K (fun x => ∑ i, f x i) :=
 by