chore(analysis/normed_space/pi_Lp): add pi_Lp.linear_equiv (#14380)

This is just a more bundled version of the `pi_Lp.equiv` we already have.
Also adds two missing simp lemmas about `pi_Lp.equiv`.

src/analysis/inner_product_space/pi_L2.lean

@@ -153,11 +153,17 @@ end
 all other coordinates. -/
 def euclidean_space.single [decidable_eq ι] (i : ι) (a : 𝕜) :
   euclidean_space 𝕜 ι :=
-pi.single i a
+(pi_Lp.equiv _ _).symm (pi.single i a)
+
+@[simp] lemma pi_Lp.equiv_single [decidable_eq ι] (i : ι) (a : 𝕜) :
+  pi_Lp.equiv _ _ (euclidean_space.single i a) = pi.single i a := rfl
+
+@[simp] lemma pi_Lp.equiv_symm_single [decidable_eq ι] (i : ι) (a : 𝕜) :
+  (pi_Lp.equiv _ _).symm (pi.single i a) = euclidean_space.single i a := rfl
 
 @[simp] theorem euclidean_space.single_apply [decidable_eq ι] (i : ι) (a : 𝕜) (j : ι) :
   (euclidean_space.single i a) j = ite (j = i) a 0 :=
-by { rw [euclidean_space.single, ← pi.single_apply i a j] }
+by { rw [euclidean_space.single, pi_Lp.equiv_symm_apply, ← pi.single_apply i a j] }
 
 lemma euclidean_space.inner_single_left [decidable_eq ι] (i : ι) (a : 𝕜) (v : euclidean_space 𝕜 ι) :
   ⟪euclidean_space.single i (a : 𝕜), v⟫ = conj a * (v i) :=

src/analysis/normed_space/pi_Lp.lean

@@ -76,7 +76,7 @@ instance fact_one_le_two_real : fact ((1:ℝ) ≤ 2) := ⟨one_le_two⟩
 
 namespace pi_Lp
 
-variables (p : ℝ) [fact_one_le_p : fact (1 ≤ p)] (α : ι → Type*) (β : ι → Type*)
+variables (p : ℝ) [fact_one_le_p : fact (1 ≤ p)] (𝕜 : Type*) (α : ι → Type*) (β : ι → Type*)
 
 /-- Canonical bijection between `pi_Lp p α` and the original Pi type. We introduce it to be able
 to compare the `L^p` and `L^∞` distances through it. -/
@@ -285,7 +285,7 @@ subtype.ext $ by { push_cast, exact norm_eq_of_L2 x }
 
 include fact_one_le_p
 
-variables (𝕜 : Type*) [normed_field 𝕜]
+variables [normed_field 𝕜]
 
 /-- The product of finitely many normed spaces is a normed space, with the `L^p` norm. -/
 instance normed_space [Π i, semi_normed_group (β i)] [Π i, normed_space 𝕜 (β i)] :
@@ -352,4 +352,13 @@ lemma norm_equiv_symm_one {β} [semi_normed_group β] [has_one β] :
   ∥(pi_Lp.equiv p (λ _ : ι, β)).symm 1∥ = fintype.card ι ^ (1 / p) * ∥(1 : β)∥ :=
 (norm_equiv_symm_const (1 : β)).trans rfl
 
+variables (𝕜)
+
+/-- `pi_Lp.equiv` as a linear map. -/
+@[simps {fully_applied := ff}]
+protected def linear_equiv : pi_Lp p β ≃ₗ[𝕜] Π i, β i :=
+{ to_fun := pi_Lp.equiv _ _,
+  inv_fun := (pi_Lp.equiv _ _).symm,
+  ..linear_equiv.refl _ _}
+
 end pi_Lp