English
The product of Haar measures is Haar, provided the component Haar measures exist on each factor.
Русский
Произведение хааровских мер на факторизованных пространствах является хааровской мерой.
LaTeX
$$$(\forall i, IsHaarMeasure(volume_i)) \Rightarrow IsHaarMeasure(volume)$$$
Lean4
/-- We intentionally restrict this only to the nondependent function space, since type-class
inference cannot find an instance for `ι → ℝ` when this is stated for dependent function spaces. -/
@[to_additive /-- We intentionally restrict this only to the nondependent function space, since
type-class inference cannot find an instance for `ι → ℝ` when this is stated for dependent function
spaces. -/
]
instance isInvInvariant_volume {α} [Group α] [MeasureSpace α] [SigmaFinite (volume : Measure α)] [MeasurableInv α]
[IsInvInvariant (volume : Measure α)] : IsInvInvariant (volume : Measure (ι → α)) :=
pi.isInvInvariant _
