feat(analysis/normed_space/basic): pi and prod are `normed_algebr…

…a`s (#13442)

Note that over an empty index type, `pi` is not a normed_algebra since it is trivial as a ring.

src/analysis/normed_space/basic.lean

@@ -348,6 +348,10 @@ class normed_algebra (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [semi_no
   [h : normed_algebra 𝕜 𝕜'] (x : 𝕜) : ∥algebra_map 𝕜 𝕜' x∥ = ∥x∥ :=
 normed_algebra.norm_algebra_map_eq _
 
+@[simp] lemma nnorm_algebra_map_eq {𝕜 : Type*} (𝕜' : Type*) [normed_field 𝕜] [semi_normed_ring 𝕜']
+  [h : normed_algebra 𝕜 𝕜'] (x : 𝕜) : ∥algebra_map 𝕜 𝕜' x∥₊ = ∥x∥₊ :=
+subtype.ext $ normed_algebra.norm_algebra_map_eq _
+
 /-- In a normed algebra, the inclusion of the base field in the extended field is an isometry. -/
 lemma algebra_map_isometry (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [semi_normed_ring 𝕜']
   [normed_algebra 𝕜 𝕜'] : isometry (algebra_map 𝕜 𝕜') :=
@@ -429,6 +433,26 @@ instance normed_algebra_rat {𝕜} [normed_division_ring 𝕜] [char_zero 𝕜]
 { norm_algebra_map_eq := λ q,
     by simpa only [ring_hom.map_rat_algebra_map] using norm_algebra_map_eq 𝕜 (algebra_map _ ℝ q) }
 
+/-- The product of two normed algebras is a normed algebra, with the sup norm. -/
+instance prod.normed_algebra {E F : Type*} [semi_normed_ring E] [semi_normed_ring F]
+  [normed_algebra 𝕜 E] [normed_algebra 𝕜 F] :
+  normed_algebra 𝕜 (E × F) :=
+{ norm_algebra_map_eq := λ x, begin
+    dsimp [prod.norm_def],
+    rw [norm_algebra_map_eq, norm_algebra_map_eq, max_self],
+  end }
+
+/-- The product of finitely many normed algebras is a normed algebra, with the sup norm. -/
+instance pi.normed_algebra {E : ι → Type*} [fintype ι] [nonempty ι]
+  [Π i, semi_normed_ring (E i)] [Π i, normed_algebra 𝕜 (E i)] :
+  normed_algebra 𝕜 (Π i, E i) :=
+{ norm_algebra_map_eq := λ x, begin
+    dsimp [has_norm.norm],
+    simp_rw [pi.algebra_map_apply ι E, nnorm_algebra_map_eq, ←coe_nnnorm],
+    rw finset.sup_const (@finset.univ_nonempty ι _ _) _,
+  end,
+  .. pi.algebra _ E }
+
 end normed_algebra
 
 section restrict_scalars

src/measure_theory/measure/haar_lebesgue.lean

@@ -195,9 +195,8 @@ begin
   /- We have already proved the result for the Lebesgue product measure, using matrices.
   We deduce it for any Haar measure by uniqueness (up to scalar multiplication). -/
   have := add_haar_measure_unique μ (pi_Icc01 ι),
-  rw this,
-  simp [add_haar_measure_eq_volume_pi, real.map_linear_map_volume_pi_eq_smul_volume_pi hf,
-    smul_smul, mul_comm],
+  rw [this, add_haar_measure_eq_volume_pi, map_smul,
+    real.map_linear_map_volume_pi_eq_smul_volume_pi hf, smul_comm],
 end
 
 lemma map_linear_map_add_haar_eq_smul_add_haar