diff --git a/Mathlib.lean b/Mathlib.lean
index 8655b95b22381..05e8a7aa6a1f1 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2612,6 +2612,7 @@ import Mathlib.MeasureTheory.Measure.Count
 import Mathlib.MeasureTheory.Measure.Dirac
 import Mathlib.MeasureTheory.Measure.Doubling
 import Mathlib.MeasureTheory.Measure.FiniteMeasure
+import Mathlib.MeasureTheory.Measure.FiniteMeasureProd
 import Mathlib.MeasureTheory.Measure.GiryMonad
 import Mathlib.MeasureTheory.Measure.Haar.Basic
 import Mathlib.MeasureTheory.Measure.Haar.Disintegration
diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
index 42e81dbc00b8a..7c505edeee1df 100644
--- a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
+++ b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
@@ -744,6 +744,9 @@ noncomputable def map (ν : FiniteMeasure Ω) (f : Ω → Ω') : FiniteMeasure 
       exact measure_lt_top (↑ν) (f ⁻¹' univ)
     · simp [Measure.map, f_aemble]⟩
 
+@[simp] lemma toMeasure_map (ν : FiniteMeasure Ω) (f : Ω → Ω') :
+    (ν.map f).toMeasure = ν.toMeasure.map f := rfl
+
 /-- Note that this is an equality of elements of `ℝ≥0∞`. See also
 `MeasureTheory.FiniteMeasure.map_apply` for the corresponding equality as elements of `ℝ≥0`. -/
 lemma map_apply' (ν : FiniteMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν)
@@ -757,7 +760,7 @@ lemma map_apply_of_aemeasurable (ν : FiniteMeasure Ω) {f : Ω → Ω'} (f_aemb
   have := ν.map_apply' f_aemble A_mble
   exact (ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr this
 
-@[simp] lemma map_apply (ν : FiniteMeasure Ω) {f : Ω → Ω'} (f_mble : Measurable f)
+lemma map_apply (ν : FiniteMeasure Ω) {f : Ω → Ω'} (f_mble : Measurable f)
     {A : Set Ω'} (A_mble : MeasurableSet A) :
     ν.map f A = ν (f ⁻¹' A) :=
   map_apply_of_aemeasurable ν f_mble.aemeasurable A_mble
@@ -765,19 +768,19 @@ lemma map_apply_of_aemeasurable (ν : FiniteMeasure Ω) {f : Ω → Ω'} (f_aemb
 @[simp] lemma map_add {f : Ω → Ω'} (f_mble : Measurable f) (ν₁ ν₂ : FiniteMeasure Ω) :
     (ν₁ + ν₂).map f = ν₁.map f + ν₂.map f := by
   ext s s_mble
-  simp [map_apply' _ f_mble.aemeasurable s_mble, toMeasure_add]
+  simp only [map_apply' _ f_mble.aemeasurable s_mble, toMeasure_add, Measure.add_apply]
 
-@[simp] lemma map_smul {f : Ω → Ω'} (f_mble : Measurable f) (c : ℝ≥0) (ν : FiniteMeasure Ω) :
+@[simp] lemma map_smul {f : Ω → Ω'} (c : ℝ≥0) (ν : FiniteMeasure Ω) :
     (c • ν).map f = c • (ν.map f) := by
-  ext s s_mble
-  simp [map_apply' _ f_mble.aemeasurable s_mble, toMeasure_smul]
+  ext s _
+  simp [toMeasure_smul]
 
 /-- The push-forward of a finite measure by a function between measurable spaces as a linear map. -/
 noncomputable def mapHom {f : Ω → Ω'} (f_mble : Measurable f) :
     FiniteMeasure Ω →ₗ[ℝ≥0] FiniteMeasure Ω' where
   toFun := fun ν ↦ ν.map f
   map_add' := map_add f_mble
-  map_smul' := map_smul f_mble
+  map_smul' := map_smul
 
 variable [TopologicalSpace Ω] [OpensMeasurableSpace Ω]
 variable [TopologicalSpace Ω'] [BorelSpace Ω']
@@ -810,7 +813,7 @@ noncomputable def mapClm {f : Ω → Ω'} (f_cont : Continuous f) :
     FiniteMeasure Ω →L[ℝ≥0] FiniteMeasure Ω' where
   toFun := fun ν ↦ ν.map f
   map_add' := map_add f_cont.measurable
-  map_smul' := map_smul f_cont.measurable
+  map_smul' := map_smul
   cont := continuous_map f_cont
 
 end map -- section
diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
new file mode 100644
index 0000000000000..ad4b11dad9e1b
--- /dev/null
+++ b/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2023 Kalle Kytölä. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kalle Kytölä
+-/
+import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
+import Mathlib.MeasureTheory.Constructions.Prod.Basic
+
+/-!
+# Products of finite measures and probability measures
+
+This file introduces binary products of finite measures and probability measures. The constructions
+are obtained from special cases of products of general measures. Taking products nevertheless has
+specific properties in the cases of finite measures and probability measures, notably the fact that
+the product measures depend continuously on their factors in the topology of weak convergence when
+the underlying space is metrizable and separable.
+
+## Main definitions
+
+* `MeasureTheory.FiniteMeasure.prod`: The product of two finite measures.
+* `MeasureTheory.ProbabilityMeasure.prod`: The product of two probability measures.
+
+## Todo
+
+* Add continuous dependence of the product measures on the factors.
+
+-/
+
+open MeasureTheory Topology Metric Filter Set ENNReal NNReal
+
+open scoped Topology ENNReal NNReal BoundedContinuousFunction BigOperators
+
+namespace MeasureTheory
+
+section FiniteMeasure_product
+
+namespace FiniteMeasure
+
+variable {α : Type*} [MeasurableSpace α] {β : Type*} [MeasurableSpace β]
+
+/-- The binary product of finite measures. -/
+noncomputable def prod (μ : FiniteMeasure α) (ν : FiniteMeasure β) : FiniteMeasure (α × β) :=
+  ⟨μ.toMeasure.prod ν.toMeasure, inferInstance⟩
+
+variable (μ : FiniteMeasure α) (ν : FiniteMeasure β)
+
+@[simp] lemma toMeasure_prod : (μ.prod ν).toMeasure = μ.toMeasure.prod ν.toMeasure := rfl
+
+lemma prod_apply (s : Set (α × β)) (s_mble : MeasurableSet s) :
+    μ.prod ν s = ENNReal.toNNReal (∫⁻ x, ν.toMeasure (Prod.mk x ⁻¹' s) ∂μ) := by
+  simp [Measure.prod_apply s_mble]
+
+lemma prod_apply_symm (s : Set (α × β)) (s_mble : MeasurableSet s) :
+    μ.prod ν s = ENNReal.toNNReal (∫⁻ y, μ.toMeasure ((fun x ↦ ⟨x, y⟩) ⁻¹' s) ∂ν) := by
+  simp [Measure.prod_apply_symm s_mble]
+
+lemma prod_prod (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) = μ s * ν t := by simp
+
+@[simp] lemma mass_prod : (μ.prod ν).mass = μ.mass * ν.mass := by
+  simp only [mass, univ_prod_univ.symm, toMeasure_prod]
+  rw [← ENNReal.toNNReal_mul]
+  exact congr_arg ENNReal.toNNReal (Measure.prod_prod univ univ)
+
+@[simp] lemma zero_prod : (0 : FiniteMeasure α).prod ν = 0 := by
+  rw [← mass_zero_iff, mass_prod, zero_mass, zero_mul]
+
+@[simp] lemma prod_zero : μ.prod (0 : FiniteMeasure β) = 0 := by
+  rw [← mass_zero_iff, mass_prod, zero_mass, mul_zero]
+
+@[simp] lemma map_fst_prod : (μ.prod ν).map Prod.fst = ν univ • μ := by
+  apply Subtype.ext
+  simp only [val_eq_toMeasure, toMeasure_map, toMeasure_prod, Measure.map_fst_prod]
+  ext s _
+  simp only [Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply, smul_eq_mul]
+  have aux := coeFn_smul_apply (ν univ) μ s
+  simpa using congr_arg ENNReal.ofNNReal aux.symm
+
+@[simp] lemma map_snd_prod : (μ.prod ν).map Prod.snd = μ univ • ν := by
+  apply Subtype.ext
+  simp only [val_eq_toMeasure, toMeasure_map, toMeasure_prod, Measure.map_fst_prod]
+  ext s _
+  simp only [Measure.map_snd_prod, Measure.smul_toOuterMeasure, OuterMeasure.coe_smul,
+    Pi.smul_apply, smul_eq_mul]
+  have aux := coeFn_smul_apply (μ univ) ν s
+  simpa using congr_arg ENNReal.ofNNReal aux.symm
+
+lemma map_prod_map {α' : Type*} [MeasurableSpace α'] {β' : Type*} [MeasurableSpace β']
+    {f : α → α'} {g : β → β'}  (f_mble : Measurable f) (g_mble : Measurable g):
+    (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g) := by
+  apply Subtype.ext
+  simp only [val_eq_toMeasure, toMeasure_prod, toMeasure_map]
+  rw [Measure.map_prod_map _ _ f_mble g_mble] <;> infer_instance
+
+lemma prod_swap : (μ.prod ν).map Prod.swap = ν.prod μ := by
+  apply Subtype.ext
+  simp [Measure.prod_swap]
+
+end FiniteMeasure -- namespace
+
+end FiniteMeasure_product -- section
+
+section ProbabilityMeasure_product
+
+namespace ProbabilityMeasure
+
+variable {α : Type*} [MeasurableSpace α] {β : Type*} [MeasurableSpace β]
+
+/-- The binary product of probability measures. -/
+noncomputable def prod (μ : ProbabilityMeasure α) (ν : ProbabilityMeasure β) :
+    ProbabilityMeasure (α × β) :=
+  ⟨μ.toMeasure.prod ν.toMeasure, by infer_instance⟩
+
+variable (μ : ProbabilityMeasure α) (ν : ProbabilityMeasure β)
+
+@[simp] lemma toMeasure_prod : (μ.prod ν).toMeasure = μ.toMeasure.prod ν.toMeasure := rfl
+
+lemma prod_apply (s : Set (α × β)) (s_mble : MeasurableSet s) :
+    μ.prod ν s = ENNReal.toNNReal (∫⁻ x, ν.toMeasure (Prod.mk x ⁻¹' s) ∂μ) := by
+  simp [Measure.prod_apply s_mble]
+
+lemma prod_apply_symm (s : Set (α × β)) (s_mble : MeasurableSet s) :
+    μ.prod ν s = ENNReal.toNNReal (∫⁻ y, μ.toMeasure ((fun x ↦ ⟨x, y⟩) ⁻¹' s) ∂ν) := by
+  simp [Measure.prod_apply_symm s_mble]
+
+lemma prod_prod (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) = μ s * ν t := by simp
+
+/-- The first marginal of a product probability measure is the first probability measure. -/
+@[simp] lemma map_fst_prod : (μ.prod ν).map measurable_fst.aemeasurable = μ := by
+  apply Subtype.ext
+  simp only [val_eq_to_measure, toMeasure_map, toMeasure_prod, Measure.map_fst_prod,
+             measure_univ, one_smul]
+
+/-- The second marginal of a product probability measure is the second probability measure. -/
+@[simp] lemma map_snd_prod : (μ.prod ν).map measurable_snd.aemeasurable = ν := by
+  apply Subtype.ext
+  simp only [val_eq_to_measure, toMeasure_map, toMeasure_prod, Measure.map_snd_prod,
+             measure_univ, one_smul]
+
+lemma map_prod_map {α' : Type*} [MeasurableSpace α'] {β' : Type*} [MeasurableSpace β']
+    {f : α → α'} {g : β → β'} (f_mble : Measurable f) (g_mble : Measurable g) :
+    (μ.map f_mble.aemeasurable).prod (ν.map g_mble.aemeasurable)
+      = (μ.prod ν).map (f_mble.prod_map g_mble).aemeasurable := by
+  apply Subtype.ext
+  simp only [val_eq_to_measure, toMeasure_prod, toMeasure_map]
+  rw [Measure.map_prod_map _ _ f_mble g_mble] <;> infer_instance
+
+lemma prod_swap : (μ.prod ν).map measurable_swap.aemeasurable = ν.prod μ := by
+  apply Subtype.ext
+  simp [Measure.prod_swap]
+
+end ProbabilityMeasure -- namespace
+
+end ProbabilityMeasure_product -- section
+
+end MeasureTheory -- namespace
diff --git a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
index 6a7e4de483338..d2d7e1cc86237 100644
--- a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
+++ b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
@@ -533,6 +533,9 @@ noncomputable def map (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble :
    ⟨by simp only [Measure.map_apply_of_aemeasurable f_aemble MeasurableSet.univ,
                   preimage_univ, measure_univ]⟩⟩
 
+@[simp] lemma toMeasure_map (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (hf : AEMeasurable f ν) :
+    (ν.map hf).toMeasure = ν.toMeasure.map f := rfl
+
 /-- Note that this is an equality of elements of `ℝ≥0∞`. See also
 `MeasureTheory.ProbabilityMeasure.map_apply` for the corresponding equality as elements of `ℝ≥0`. -/
 lemma map_apply' (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν)
@@ -546,7 +549,7 @@ lemma map_apply_of_aemeasurable (ν : ProbabilityMeasure Ω) {f : Ω → Ω'}
   have := ν.map_apply' f_aemble A_mble
   exact (ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr this
 
-@[simp] lemma map_apply (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν)
+lemma map_apply (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν)
     {A : Set Ω'} (A_mble : MeasurableSet A) :
     (ν.map f_aemble) A = ν (f ⁻¹' A) :=
   map_apply_of_aemeasurable ν f_aemble A_mble