Unique

📁 Source: Mathlib/MeasureTheory/Measure/Haar/Unique.lean

Statistics

Metric	Count
Definitions `addHaarScalarFactor`, `haarScalarFactor`	2
Theorems `measurePreserving`, `isNegInvariant_of_innerRegular`, `isNegInvariant_of_regular`, `isInvInvariant_of_innerRegular`, `isInvInvariant_of_regular`, `zpow`, `zsmul`, `absolutelyContinuous_isAddHaarMeasure`, `absolutelyContinuous_isHaarMeasure`, `addHaarScalarFactor_domSMul`, `addHaarScalarFactor_eq_integral_div`, `addHaarScalarFactor_eq_mul`, `addHaarScalarFactor_pos_of_isAddHaarMeasure`, `addHaarScalarFactor_self`, `addHaarScalarFactor_smul`, `addHaarScalarFactor_smul_congr`, `addHaarScalarFactor_smul_congr'`, `addHaarScalarFactor_smul_smul`, `exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport`, `exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport`, `haarScalarFactor_eq_integral_div`, `haarScalarFactor_eq_mul`, `haarScalarFactor_pos_of_isHaarMeasure`, `haarScalarFactor_self`, `haarScalarFactor_smul`, `haarScalarFactor_smul_smul`, `instInnerRegularOfIsAddHaarMeasureOfCompactSpace`, `instInnerRegularOfIsHaarMeasureOfCompactSpace`, `instRegularOfIsAddHaarMeasureOfCompactSpace`, `instRegularOfIsHaarMeasureOfCompactSpace`, `integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport`, `integral_isAddLeftInvariant_isAddRightInvariant_combo`, `integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport`, `integral_isMulLeftInvariant_isMulRightInvariant_combo`, `isAddHaarMeasure_eq_of_isProbabilityMeasure`, `isAddInvariant_eq_smul_of_compactSpace`, `isAddLeftInvariant_eq_smul`, `isAddLeftInvariant_eq_smul_of_innerRegular`, `isAddLeftInvariant_eq_smul_of_regular`, `isHaarMeasure_eq_of_isProbabilityMeasure`, `isMulInvariant_eq_smul_of_compactSpace`, `isMulLeftInvariant_eq_smul`, `isMulLeftInvariant_eq_smul_of_innerRegular`, `isMulLeftInvariant_eq_smul_of_regular`, `measurePreserving_zpow`, `measurePreserving_zsmul`, `measure_isAddHaarMeasure_eq_smul_of_isEverywherePos`, `measure_isAddHaarMeasure_eq_smul_of_isOpen`, `measure_isAddInvariant_eq_smul_of_isCompact_closure`, `measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop`, `measure_isAddInvariant_eq_smul_of_isCompact_closure_of_measurableSet`, `measure_isAddLeftInvariant_eq_vadd_of_ne_top`, `measure_isHaarMeasure_eq_smul_of_isEverywherePos`, `measure_isHaarMeasure_eq_smul_of_isOpen`, `measure_isMulInvariant_eq_smul_of_isCompact_closure`, `measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop`, `measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet`, `measure_isMulLeftInvariant_eq_smul_of_ne_top`, `measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport`, `measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport`, `mul_addHaarScalarFactor_smul`, `mul_haarScalarFactor_smul`, `smul_measure_isAddInvariant_le_of_isCompact_closure`, `smul_measure_isMulInvariant_le_of_isCompact_closure`, `continuous_integral_apply_inv_mul`, `continuous_integral_apply_neg_add`, `measurePreserving`	67
Total	69

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurePreserving` 📖	mathematical	`Continuous` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.univ`	`MeasureTheory.MeasurePreserving`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `MeasureTheory.measure_lt_top` `MeasureTheory.CompactSpace.isFiniteMeasure` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.isAddHaarMeasure_map_of_isFiniteMeasure` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant` `IsScalarTower.right` `MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_innerRegular` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `IsTopologicalAddGroup.regularSpace` `instWeaklyLocallyCompactSpaceOfCompactSpace` `MeasureTheory.Measure.instInnerRegularOfIsAddHaarMeasureOfCompactSpace` `one_mul` `smul_eq_mul` `ENNReal.smul_def` `MeasureTheory.Measure.smul_apply` `MeasureTheory.Measure.map_apply` `MeasurableSet.univ` `Set.preimage_univ` `ENNReal.coe_eq_one` `MeasureTheory.Measure.instNeZeroENNRealCoeSetUniv` `MeasureTheory.Measure.instNeZeroOfNonempty` `MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure` `Zero.instNonempty` `MeasureTheory.measure_ne_top` `one_smul`

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_integral_apply_inv_mul` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `HasCompactSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`integral` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`continuous_iff_continuousAt` `WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `IsCompact.smul_set` `ContinuousMul.to_continuousSMul` `IsTopologicalGroup.toContinuousMul` `IsCompact.inv` `IsTopologicalGroup.toContinuousInv` `continuousOn_integral_of_compact_support` `BorelSpace.opensMeasurable` `Continuous.continuousOn` `Continuous.comp` `Continuous.mul` `Continuous.inv` `continuous_snd` `continuous_fst` `Mathlib.Tactic.Contrapose.contrapose₂` `mul_inv_rev` `inv_inv` `subset_tsupport` `mul_inv_cancel_left` `ContinuousOn.continuousAt`
`continuous_integral_apply_neg_add` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `HasCompactSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`integral` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `AddGroup.toSubtractionMonoid`	—	`continuous_iff_continuousAt` `WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `IsCompact.vadd_set` `ContinuousAdd.to_continuousVAdd` `IsTopologicalAddGroup.toContinuousAdd` `IsCompact.neg` `IsTopologicalAddGroup.toContinuousNeg` `continuousOn_integral_of_compact_support` `BorelSpace.opensMeasurable` `Continuous.continuousOn` `Continuous.comp` `Continuous.add` `Continuous.neg` `continuous_snd` `continuous_fst` `Mathlib.Tactic.Contrapose.contrapose₂` `Set.mem_neg` `neg_add_rev` `neg_neg` `subset_tsupport` `add_neg_cancel_left` `ContinuousOn.continuousAt`

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`addHaarScalarFactor` 📖	CompOp	29 math math: `isAddInvariant_eq_smul_of_compactSpace`, `MeasureTheory.addHaarScalarFactor_smul_inv_eq_distribHaarChar`, `addHaarScalarFactor_eq_integral_div`, `MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar_inv`, `integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport`, `MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar`, `smul_measure_isAddInvariant_le_of_isCompact_closure`, `measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport`, `addHaarScalarFactor_smul_congr`, `MeasureTheory.addEquivAddHaarChar_eq`, `addModularCharacterFun_eq_addHaarScalarFactor`, `MeasureTheory.distribHaarChar_apply`, `addHaarScalarFactor_eq_mul`, `measure_isAddHaarMeasure_eq_smul_of_isOpen`, `measure_isAddInvariant_eq_smul_of_isCompact_closure`, `addHaarScalarFactor_smul_smul`, `measure_isAddHaarMeasure_eq_smul_of_isEverywherePos`, `measure_isAddLeftInvariant_eq_vadd_of_ne_top`, `mul_addHaarScalarFactor_smul`, `isAddLeftInvariant_eq_smul_of_regular`, `isAddLeftInvariant_eq_smul_of_innerRegular`, `addHaarScalarFactor_domSMul`, `measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop`, `addHaarScalarFactor_smul_congr'`, `measure_isAddInvariant_eq_smul_of_isCompact_closure_of_measurableSet`, `addHaarScalarFactor_pos_of_isAddHaarMeasure`, `isAddLeftInvariant_eq_smul`, `addHaarScalarFactor_smul`, `addHaarScalarFactor_self`
`haarScalarFactor` 📖	CompOp	22 math math: `measure_isMulLeftInvariant_eq_smul_of_ne_top`, `haarScalarFactor_pos_of_isHaarMeasure`, `MeasureTheory.mulEquivHaarChar_eq`, `haarScalarFactor_smul`, `isMulLeftInvariant_eq_smul_of_innerRegular`, `isMulLeftInvariant_eq_smul_of_regular`, `measure_isMulInvariant_eq_smul_of_isCompact_closure`, `isMulInvariant_eq_smul_of_compactSpace`, `measure_isHaarMeasure_eq_smul_of_isEverywherePos`, `haarScalarFactor_eq_integral_div`, `smul_measure_isMulInvariant_le_of_isCompact_closure`, `measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet`, `integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport`, `isMulLeftInvariant_eq_smul`, `measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport`, `haarScalarFactor_smul_smul`, `haarScalarFactor_self`, `mul_haarScalarFactor_smul`, `haarScalarFactor_eq_mul`, `measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop`, `modularCharacterFun_eq_haarScalarFactor`, `measure_isHaarMeasure_eq_smul_of_isOpen`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absolutelyContinuous_isAddHaarMeasure` 📖	mathematical	—	`AbsolutelyContinuous`	—	`TopologicalSpace.PositiveCompacts.nonempty'` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `Zero.instNonempty` `IsScalarTower.right` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `isAddHaarMeasure_addHaarMeasure` `isAddLeftInvariant_addHaarMeasure` `isAddLeftInvariant_eq_smul` `addHaarMeasure_unique` `smul_smul` `smul_absolutelyContinuous`
`absolutelyContinuous_isHaarMeasure` 📖	mathematical	—	`AbsolutelyContinuous`	—	`TopologicalSpace.PositiveCompacts.nonempty'` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `One.instNonempty` `IsScalarTower.right` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `isHaarMeasure_haarMeasure` `isMulLeftInvariant_haarMeasure` `isMulLeftInvariant_eq_smul` `haarMeasure_unique` `smul_smul` `smul_absolutelyContinuous`
`addHaarScalarFactor_domSMul` 📖	mathematical	—	`addHaarScalarFactor` `AddCommGroup.toAddGroup` `DomMulAct` `MeasureTheory.Measure` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DomMulAct.instMonoidOfMulOpposite` `MulOpposite.instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instDistribMulActionDomMulAct` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ContinuousConstSMul.toMeasurableConstSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `IsAddHaarMeasure.domSMul` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant`	—	`ContinuousConstSMul.toMeasurableConstSMul` `IsAddHaarMeasure.domSMul` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant` `exists_continuous_nonneg_pos` `IsTopologicalAddGroup.regularSpace` `LT.lt.ne'` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `BorelSpace.opensMeasurable` `IsAddHaarMeasure.toIsOpenPosMeasure` `NNReal.coe_injective` `addHaarScalarFactor_eq_integral_div` `MeasureTheory.integral_domSMul` `Continuous.comp'` `Continuous.const_smul` `continuous_id'` `HasCompactSupport.comp_isClosedEmbedding` `Homeomorph.isClosedEmbedding`
`addHaarScalarFactor_eq_integral_div` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasCompactSupport` `Real.instZero`	`NNReal.toReal` `addHaarScalarFactor` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal`	—	`IsScalarTower.right` `integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport` `EuclideanDomain.eq_div_of_mul_eq_left` `MeasureTheory.integral_smul_nnreal_measure`
`addHaarScalarFactor_eq_mul` 📖	mathematical	—	`addHaarScalarFactor` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant`	—	`IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant` `exists_continuous_nonneg_pos` `IsTopologicalAddGroup.regularSpace` `IsScalarTower.right` `integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport` `MeasureTheory.integral_pos_iff_support_of_nonneg` `Continuous.integrable_of_hasCompactSupport` `BorelSpace.opensMeasurable` `IsOpen.measure_pos` `IsAddHaarMeasure.toIsOpenPosMeasure` `Continuous.isOpen_support` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `mul_eq_mul_right_iff` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `NNReal.eq_iff` `LT.lt.ne'` `MeasureTheory.integral_smul_nnreal_measure` `smul_smul` `exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport` `mul_one`
`addHaarScalarFactor_pos_of_isAddHaarMeasure` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `addHaarScalarFactor` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant`	—	`IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant` `pos_iff_ne_zero` `NNReal.instCanonicallyOrderedAdd` `addHaarScalarFactor_self` `MulZeroClass.zero_mul` `one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `addHaarScalarFactor_eq_mul`
`addHaarScalarFactor_self` 📖	mathematical	—	`addHaarScalarFactor` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant` `NNReal` `instOneNNReal`	—	`IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant` `exists_continuous_nonneg_pos` `IsTopologicalAddGroup.regularSpace` `ne_of_gt` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `BorelSpace.opensMeasurable` `IsAddHaarMeasure.toIsOpenPosMeasure` `NNReal.coe_injective` `addHaarScalarFactor_eq_integral_div` `div_self` `exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport`
`addHaarScalarFactor_smul` 📖	mathematical	—	`addHaarScalarFactor` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `MeasureTheory.isAddLeftInvariant_smul_nnreal` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`IsScalarTower.right` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `MeasureTheory.isAddLeftInvariant_smul_nnreal` `exists_continuous_nonneg_pos` `IsTopologicalAddGroup.regularSpace` `ne_of_gt` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `BorelSpace.opensMeasurable` `IsAddHaarMeasure.toIsOpenPosMeasure` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `NNReal.coe_injective` `addHaarScalarFactor_eq_integral_div` `MeasureTheory.integral_smul_nnreal_measure` `smul_div_assoc`
`addHaarScalarFactor_smul_congr` 📖	mathematical	—	`addHaarScalarFactor` `AddCommGroup.toAddGroup` `DomMulAct` `MeasureTheory.Measure` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DomMulAct.instMonoidOfMulOpposite` `MulOpposite.instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instDistribMulActionDomMulAct` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ContinuousConstSMul.toMeasurableConstSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `IsAddHaarMeasure.domSMul` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant`	—	`ContinuousConstSMul.toMeasurableConstSMul` `IsAddHaarMeasure.domSMul` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant` `addHaarScalarFactor_eq_mul` `addHaarScalarFactor_domSMul` `mul_comm`
`addHaarScalarFactor_smul_congr'` 📖	mathematical	—	`addHaarScalarFactor` `AddCommGroup.toAddGroup` `DomMulAct` `MeasureTheory.Measure` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DomMulAct.instMonoidOfMulOpposite` `MulOpposite.instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instDistribMulActionDomMulAct` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ContinuousConstSMul.toMeasurableConstSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.domSMul` `IsAddHaarMeasure.toIsAddLeftInvariant`	—	`ContinuousConstSMul.toMeasurableConstSMul` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.domSMul` `IsAddHaarMeasure.toIsAddLeftInvariant` `addHaarScalarFactor_eq_mul` `addHaarScalarFactor_domSMul` `mul_comm`
`addHaarScalarFactor_smul_smul` 📖	mathematical	—	`addHaarScalarFactor` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `IsAddHaarMeasure.nnreal_smul` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `MeasureTheory.isAddLeftInvariant_smul_nnreal` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`IsScalarTower.right` `IsAddHaarMeasure.nnreal_smul` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `MeasureTheory.isAddLeftInvariant_smul_nnreal` `addHaarScalarFactor_smul` `smul_eq_mul` `mul_addHaarScalarFactor_smul`
`exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport` 📖	mathematical	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `exists_continuous_nonneg_pos` `IsTopologicalAddGroup.regularSpace` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `BorelSpace.opensMeasurable` `IsAddHaarMeasure.toIsOpenPosMeasure` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `inv_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MeasureTheory.integral_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `integral_isAddLeftInvariant_isAddRightInvariant_combo` `IsFiniteMeasureOnCompacts.neg` `IsTopologicalAddGroup.toContinuousNeg` `IsAddHaarMeasure.toIsAddLeftInvariant` `neg.instIsAddRightInvariant` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousNeg.measurableNeg` `IsOpenPosMeasure.neg` `mul_comm` `mul_assoc` `mul_inv_eq_iff_eq_mul₀` `LT.lt.ne'` `MeasureTheory.integral_smul_nnreal_measure` `HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `MeasureTheory.integral_zero` `zero_smul`
`exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport` 📖	mathematical	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `exists_continuous_nonneg_pos` `IsTopologicalGroup.regularSpace` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `BorelSpace.opensMeasurable` `IsHaarMeasure.toIsOpenPosMeasure` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `inv_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MeasureTheory.integral_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `integral_isMulLeftInvariant_isMulRightInvariant_combo` `IsFiniteMeasureOnCompacts.inv` `IsTopologicalGroup.toContinuousInv` `IsHaarMeasure.toIsMulLeftInvariant` `inv.instIsMulRightInvariant` `ContinuousMul.measurableMul` `IsTopologicalGroup.toContinuousMul` `ContinuousInv.measurableInv` `IsOpenPosMeasure.inv` `mul_comm` `mul_assoc` `mul_inv_eq_iff_eq_mul₀` `LT.lt.ne'` `MeasureTheory.integral_smul_nnreal_measure` `HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `MeasureTheory.integral_zero` `zero_smul`
`haarScalarFactor_eq_integral_div` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasCompactSupport` `Real.instZero`	`NNReal.toReal` `haarScalarFactor` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal`	—	`IsScalarTower.right` `integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport` `EuclideanDomain.eq_div_of_mul_eq_left` `MeasureTheory.integral_smul_nnreal_measure`
`haarScalarFactor_eq_mul` 📖	mathematical	—	`haarScalarFactor` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `IsHaarMeasure.toIsMulLeftInvariant`	—	`IsHaarMeasure.toIsFiniteMeasureOnCompacts` `IsHaarMeasure.toIsMulLeftInvariant` `exists_continuous_nonneg_pos` `IsTopologicalGroup.regularSpace` `IsScalarTower.right` `integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport` `MeasureTheory.integral_pos_iff_support_of_nonneg` `Continuous.integrable_of_hasCompactSupport` `BorelSpace.opensMeasurable` `IsOpen.measure_pos` `IsHaarMeasure.toIsOpenPosMeasure` `Continuous.isOpen_support` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `mul_eq_mul_right_iff` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `LT.lt.ne'` `MeasureTheory.integral_smul_nnreal_measure` `smul_smul` `exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport` `mul_one`
`haarScalarFactor_pos_of_isHaarMeasure` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `haarScalarFactor` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `IsHaarMeasure.toIsMulLeftInvariant`	—	`IsHaarMeasure.toIsFiniteMeasureOnCompacts` `IsHaarMeasure.toIsMulLeftInvariant` `pos_iff_ne_zero` `NNReal.instCanonicallyOrderedAdd` `haarScalarFactor_self` `MulZeroClass.zero_mul` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `haarScalarFactor_eq_mul`
`haarScalarFactor_self` 📖	mathematical	—	`haarScalarFactor` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `IsHaarMeasure.toIsMulLeftInvariant` `NNReal` `instOneNNReal`	—	`IsHaarMeasure.toIsFiniteMeasureOnCompacts` `IsHaarMeasure.toIsMulLeftInvariant` `exists_continuous_nonneg_pos` `IsTopologicalGroup.regularSpace` `ne_of_gt` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `BorelSpace.opensMeasurable` `IsHaarMeasure.toIsOpenPosMeasure` `NNReal.coe_injective` `haarScalarFactor_eq_integral_div` `div_self` `exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport`
`haarScalarFactor_smul` 📖	mathematical	—	`haarScalarFactor` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `MeasureTheory.isMulLeftInvariant_smul_nnreal` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`IsScalarTower.right` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `MeasureTheory.isMulLeftInvariant_smul_nnreal` `exists_continuous_nonneg_pos` `IsTopologicalGroup.regularSpace` `ne_of_gt` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `BorelSpace.opensMeasurable` `IsHaarMeasure.toIsOpenPosMeasure` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `NNReal.coe_injective` `haarScalarFactor_eq_integral_div` `MeasureTheory.integral_smul_nnreal_measure` `smul_div_assoc`
`haarScalarFactor_smul_smul` 📖	mathematical	—	`haarScalarFactor` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `IsHaarMeasure.nnreal_smul` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `MeasureTheory.isMulLeftInvariant_smul_nnreal` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`IsScalarTower.right` `IsHaarMeasure.nnreal_smul` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `MeasureTheory.isMulLeftInvariant_smul_nnreal` `haarScalarFactor_smul` `smul_eq_mul` `mul_haarScalarFactor_smul`
`instInnerRegularOfIsAddHaarMeasureOfCompactSpace` 📖	mathematical	—	`InnerRegular`	—	`IsScalarTower.right` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `IsTopologicalAddGroup.regularSpace` `instWeaklyLocallyCompactSpaceOfCompactSpace` `isAddHaarMeasure_addHaarMeasure` `isAddInvariant_eq_smul_of_compactSpace` `InnerRegular.smul_nnreal` `InnerRegularCompactLTTop.instInnerRegularOfSigmaFinite` `Regular.instInnerRegularCompactLTTop` `regular_addHaarMeasure` `IsAddHaarMeasure.sigmaFinite` `CompactSpace.sigmaCompact`
`instInnerRegularOfIsHaarMeasureOfCompactSpace` 📖	mathematical	—	`InnerRegular`	—	`IsScalarTower.right` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `IsTopologicalGroup.regularSpace` `instWeaklyLocallyCompactSpaceOfCompactSpace` `isHaarMeasure_haarMeasure` `isMulInvariant_eq_smul_of_compactSpace` `InnerRegular.smul_nnreal` `InnerRegularCompactLTTop.instInnerRegularOfSigmaFinite` `Regular.instInnerRegularCompactLTTop` `regular_haarMeasure` `IsHaarMeasure.sigmaFinite` `CompactSpace.sigmaCompact`
`instRegularOfIsAddHaarMeasureOfCompactSpace` 📖	mathematical	—	`Regular`	—	`IsScalarTower.right` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `IsTopologicalAddGroup.regularSpace` `instWeaklyLocallyCompactSpaceOfCompactSpace` `isAddHaarMeasure_addHaarMeasure` `isAddInvariant_eq_smul_of_compactSpace` `Regular.smul_nnreal` `regular_addHaarMeasure`
`instRegularOfIsHaarMeasureOfCompactSpace` 📖	mathematical	—	`Regular`	—	`IsScalarTower.right` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `IsTopologicalGroup.regularSpace` `instWeaklyLocallyCompactSpaceOfCompactSpace` `isHaarMeasure_haarMeasure` `isMulInvariant_eq_smul_of_compactSpace` `Regular.smul_nnreal` `regular_haarMeasure`
`integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasCompactSupport` `Real.instZero`	`MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `addHaarScalarFactor`	—	`IsScalarTower.right` `HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `MeasureTheory.integral_zero` `exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport`
`integral_isAddLeftInvariant_isAddRightInvariant_combo` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasCompactSupport` `Real.instZero` `Pi.hasLe` `Real.instLE` `Pi.instZero`	`MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instMul` `Real.instInv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `MeasureTheory.integral_zero` `MulZeroClass.zero_mul` `MeasureTheory.continuous_integral_apply_neg_add` `Continuous.comp'` `Continuous.fun_add` `IsTopologicalAddGroup.toContinuousAdd` `continuous_id'` `continuous_const` `ContinuousNeg.continuous_neg` `IsTopologicalAddGroup.toContinuousNeg` `MeasureTheory.integral_pos_iff_support_of_nonneg` `Continuous.integrable_of_hasCompactSupport` `BorelSpace.opensMeasurable` `HasCompactSupport.comp_homeomorph` `IsOpen.measure_pos` `Continuous.isOpen_support` `Function.mem_support` `neg_add_rev` `neg_neg` `neg_add_cancel_right` `mul_assoc` `inv_mul_cancel₀` `LT.lt.ne'` `mul_one` `MeasureTheory.integral_const_mul` `MeasureTheory.integral_integral_swap_of_hasCompactSupport` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.comp` `continuous_fst` `Continuous.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `Continuous.add` `Continuous.neg` `continuous_snd` `IsCompact.image` `IsCompact.prod` `IsCompact.closure` `instR1Space` `IsTopologicalAddGroup.regularSpace` `image_eq_zero_of_notMem_tsupport` `Mathlib.Tactic.Contrapose.contrapose₄` `Set.mem_prod` `subset_closure` `Set.mem_image` `neg_one_zsmul` `neg_one_zsmul_add` `mul_zsmul'` `one_zsmul` `add_assoc` `one_add_zsmul` `add_neg_cancel` `zero_zsmul` `zero_add` `MulZeroClass.mul_zero` `HasCompactSupport.intro'` `IsClosed.prod` `isClosed_tsupport` `isClosed_closure` `MeasureTheory.integral_add_left_eq_self` `ContinuousAdd.measurableAdd` `neg_add_cancel_left` `Mathlib.Tactic.Group.zsmul_trick_zero` `neg_add_cancel` `add_zero` `MeasureTheory.integral_mul_const` `MeasureTheory.integral_add_right_eq_self`
`integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasCompactSupport` `Real.instZero`	`MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `haarScalarFactor`	—	`IsScalarTower.right` `HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `MeasureTheory.integral_zero` `exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport`
`integral_isMulLeftInvariant_isMulRightInvariant_combo` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasCompactSupport` `Real.instZero` `Pi.hasLe` `Real.instLE` `Pi.instZero`	`MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instMul` `Real.instInv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `MeasureTheory.integral_zero` `MulZeroClass.zero_mul` `MeasureTheory.continuous_integral_apply_inv_mul` `Continuous.comp'` `Continuous.fun_mul` `IsTopologicalGroup.toContinuousMul` `continuous_id'` `continuous_const` `ContinuousInv.continuous_inv` `IsTopologicalGroup.toContinuousInv` `MeasureTheory.integral_pos_iff_support_of_nonneg` `Continuous.integrable_of_hasCompactSupport` `BorelSpace.opensMeasurable` `HasCompactSupport.comp_homeomorph` `IsOpen.measure_pos` `Continuous.isOpen_support` `mul_inv_rev` `inv_inv` `inv_mul_cancel_right` `mul_assoc` `inv_mul_cancel₀` `LT.lt.ne'` `mul_one` `MeasureTheory.integral_const_mul` `MeasureTheory.integral_integral_swap_of_hasCompactSupport` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.comp` `continuous_fst` `Continuous.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `Continuous.inv` `continuous_snd` `IsCompact.image` `IsCompact.prod` `IsCompact.closure` `instR1Space` `IsTopologicalGroup.regularSpace` `image_eq_zero_of_notMem_tsupport` `Mathlib.Tactic.Contrapose.contrapose₄` `subset_closure` `mul_zpow_neg_one` `neg_neg` `zpow_one` `add_neg_cancel` `zpow_zero` `one_mul` `MulZeroClass.mul_zero` `HasCompactSupport.intro'` `IsClosed.prod` `isClosed_tsupport` `isClosed_closure` `MeasureTheory.integral_mul_left_eq_self` `ContinuousMul.measurableMul` `inv_mul_cancel_left` `Mathlib.Tactic.Group.zpow_trick_one` `neg_add_cancel` `MeasureTheory.integral_mul_const` `MeasureTheory.integral_mul_right_eq_self`
`isAddHaarMeasure_eq_of_isProbabilityMeasure` 📖	—	—	—	—	`MeasureTheory.IsProbabilityMeasure.measure_univ` `ENNReal.one_ne_top` `MeasureTheory.measure_univ_of_isAddLeftInvariant` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `not_compactSpace_iff` `IsAddHaarMeasure.toIsOpenPosMeasure` `IsAddHaarMeasure.toIsAddLeftInvariant` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `measure_isAddInvariant_eq_smul_of_isCompact_closure` `IsClosed.isCompact` `isClosed_closure` `ext` `mul_one` `ENNReal.one_eq_coe` `one_smul`
`isAddInvariant_eq_smul_of_compactSpace` 📖	mathematical	—	`NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `addHaarScalarFactor`	—	`ext` `IsScalarTower.right` `measure_isAddInvariant_eq_smul_of_isCompact_closure` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `IsTopologicalAddGroup.regularSpace` `instWeaklyLocallyCompactSpaceOfCompactSpace` `IsClosed.isCompact` `isClosed_closure`
`isAddLeftInvariant_eq_smul` 📖	mathematical	—	`NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `addHaarScalarFactor`	—	`isAddLeftInvariant_eq_smul_of_regular` `Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure` `TopologicalSpace.PseudoMetrizableSpace.of_regularSpace_secondCountableTopology` `IsTopologicalAddGroup.regularSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts`
`isAddLeftInvariant_eq_smul_of_innerRegular` 📖	mathematical	—	`NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `addHaarScalarFactor`	—	`ext` `IsScalarTower.right` `MeasurableSet.measure_eq_iSup_isCompact` `InnerRegular.smul_nnreal` `iSup_congr_Prop` `measure_isAddLeftInvariant_eq_vadd_of_ne_top` `InnerRegular.instInnerRegularCompactLTTop` `LT.lt.ne` `IsCompact.measure_lt_top` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts`
`isAddLeftInvariant_eq_smul_of_regular` 📖	mathematical	—	`NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `addHaarScalarFactor`	—	`IsScalarTower.right` `IsOpen.measure_eq_iSup_isCompact` `Regular.smul_nnreal` `iSup_congr_Prop` `measure_isAddLeftInvariant_eq_vadd_of_ne_top` `Regular.instInnerRegularCompactLTTop` `LT.lt.ne` `IsCompact.measure_lt_top` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `ext` `Set.measure_eq_iInf_isOpen` `WeaklyRegular.toOuterRegular` `Regular.weaklyRegular` `instR1Space` `IsTopologicalAddGroup.regularSpace` `OuterRegular.smul_nnreal` `iInf_congr_Prop`
`isHaarMeasure_eq_of_isProbabilityMeasure` 📖	—	—	—	—	`MeasureTheory.IsProbabilityMeasure.measure_univ` `MeasureTheory.measure_univ_of_isMulLeftInvariant` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `not_compactSpace_iff` `IsHaarMeasure.toIsOpenPosMeasure` `IsHaarMeasure.toIsMulLeftInvariant` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `measure_isMulInvariant_eq_smul_of_isCompact_closure` `IsClosed.isCompact` `isClosed_closure` `ext` `mul_one` `one_smul`
`isMulInvariant_eq_smul_of_compactSpace` 📖	mathematical	—	`NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `haarScalarFactor`	—	`ext` `IsScalarTower.right` `measure_isMulInvariant_eq_smul_of_isCompact_closure` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `IsTopologicalGroup.regularSpace` `instWeaklyLocallyCompactSpaceOfCompactSpace` `IsClosed.isCompact` `isClosed_closure`
`isMulLeftInvariant_eq_smul` 📖	mathematical	—	`NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `haarScalarFactor`	—	`isMulLeftInvariant_eq_smul_of_regular` `Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure` `TopologicalSpace.PseudoMetrizableSpace.of_regularSpace_secondCountableTopology` `IsTopologicalGroup.regularSpace` `SeparableWeaklyLocallyCompactGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `IsHaarMeasure.toIsFiniteMeasureOnCompacts`
`isMulLeftInvariant_eq_smul_of_innerRegular` 📖	mathematical	—	`NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `haarScalarFactor`	—	`ext` `IsScalarTower.right` `MeasurableSet.measure_eq_iSup_isCompact` `InnerRegular.smul_nnreal` `iSup_congr_Prop` `measure_isMulLeftInvariant_eq_smul_of_ne_top` `InnerRegular.instInnerRegularCompactLTTop` `LT.lt.ne` `IsCompact.measure_lt_top` `IsHaarMeasure.toIsFiniteMeasureOnCompacts`
`isMulLeftInvariant_eq_smul_of_regular` 📖	mathematical	—	`NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `haarScalarFactor`	—	`IsScalarTower.right` `IsOpen.measure_eq_iSup_isCompact` `Regular.smul_nnreal` `iSup_congr_Prop` `measure_isMulLeftInvariant_eq_smul_of_ne_top` `Regular.instInnerRegularCompactLTTop` `LT.lt.ne` `IsCompact.measure_lt_top` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `ext` `Set.measure_eq_iInf_isOpen` `WeaklyRegular.toOuterRegular` `Regular.weaklyRegular` `instR1Space` `IsTopologicalGroup.regularSpace` `OuterRegular.smul_nnreal` `iInf_congr_Prop`
`measurePreserving_zpow` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`MonoidHom.measurePreserving` `continuous_zpow` `RootableBy.surjective_pow`
`measurePreserving_zsmul` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`AddMonoidHom.measurePreserving` `continuous_zsmul` `DivisibleBy.surjective_smul`
`measure_isAddHaarMeasure_eq_smul_of_isEverywherePos` 📖	mathematical	`MeasurableSet` `IsEverywherePos`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `addHaarScalarFactor` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant`	—	`IsScalarTower.right` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant` `WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `IsCompact.closure` `instR1Space` `IsTopologicalAddGroup.regularSpace` `isClosed_closure` `Filter.mem_of_superset` `subset_closure` `mem_of_mem_nhds` `zorn_subset` `Set.iUnion_subset_iff` `Set.mem_iUnion` `IsChain.directedOn` `Set.instReflSubset` `Set.subset_biUnion_of_mem` `Maximal.prop` `Maximal.mem_of_prop_insert` `Set.union_singleton` `neg_zero` `add_zero` `mem_leftAddCoset` `Set.add_mem_add` `Set.neg_mem_neg` `Set.mem_biUnion` `Set.insert_subset_iff` `Set.pairwiseDisjoint_insert` `Set.not_disjoint_iff` `neg_one_zsmul` `neg_one_zsmul_add` `mul_zsmul'` `mul_one` `neg_neg` `one_zsmul` `add_assoc` `Mathlib.Tactic.Group.zsmul_trick_zero` `neg_add_cancel` `zero_zsmul` `one_add_zsmul` `add_neg_cancel` `zero_add` `mem_leftAddCoset_iff` `Set.eq_empty_or_nonempty` `Set.iUnion_congr_Prop` `Set.mem_empty_iff_false` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.subset_empty_iff` `MeasureTheory.measure_empty` `instOuterMeasureClass` `Set.Countable.exists_eq_range` `MeasurableSet.disjointed` `MeasurableSet.inter` `IsClosed.vadd_left_of_isCompact` `IsTopologicalAddGroup.toContinuousNeg` `ContinuousAdd.to_continuousVAdd` `IsTopologicalAddGroup.toContinuousAdd` `IsClosed.neg` `IsClosed.measurableSet` `BorelSpace.opensMeasurable` `IsClosed.vadd` `VAddAssocClass.continuousConstVAdd` `VAddAssocClass.left` `Set.inter_iUnion` `Set.inter_eq_left` `Set.mem_range` `Set.iUnion_exists` `Set.iUnion_iUnion_eq'` `MeasureTheory.measure_iUnion` `instCountableNat` `disjoint_disjointed` `iUnion_disjointed` `measure_isAddInvariant_eq_smul_of_isCompact_closure` `IsCompact.vadd` `IsCompact.add` `IsCompact.neg` `IsCompact.closure_of_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `disjointed_subset` `Set.inter_subset_right` `Mathlib.Tactic.Contrapose.contrapose₂` `lt_of_le_of_lt` `MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint` `Set.PairwiseDisjoint.mono` `Set.Pairwise.on_injective` `Subtype.val_injective` `MeasureTheory.measure_mono` `Set.iUnion_coe_set` `Set.inter_subset_left` `Ne.lt_top` `Summable.countable_support_ennreal` `LT.lt.ne` `Set.eq_univ_iff_forall` `ne_of_gt` `inter_mem_nhdsWithin` `vadd_mem_nhds_self` `Set.countable_univ_iff` `Set.to_countable` `IsEverywherePos.smul_measure_nnreal` `LT.lt.ne'` `addHaarScalarFactor_pos_of_isAddHaarMeasure` `IsEverywherePos.of_forall_exists_nhds_eq`
`measure_isAddHaarMeasure_eq_smul_of_isOpen` 📖	mathematical	`IsOpen`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `addHaarScalarFactor` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant`	—	`measure_isAddHaarMeasure_eq_smul_of_isEverywherePos` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `IsOpen.isEverywherePos` `IsAddHaarMeasure.toIsOpenPosMeasure`
`measure_isAddInvariant_eq_smul_of_isCompact_closure` 📖	mathematical	`IsCompact` `closure`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `addHaarScalarFactor`	—	`IsScalarTower.right` `le_antisymm` `MeasureTheory.measure_mono` `instOuterMeasureClass` `Set.subset_inter` `MeasureTheory.subset_toMeasurable` `subset_closure` `measure_isAddInvariant_eq_smul_of_isCompact_closure_of_measurableSet` `MeasurableSet.inter` `MeasureTheory.measurableSet_toMeasurable` `IsClosed.measurableSet` `BorelSpace.opensMeasurable` `isClosed_closure` `IsCompact.closure_of_subset` `instR1Space` `IsTopologicalAddGroup.regularSpace` `Set.inter_subset_right` `Set.inter_subset_left` `MeasureTheory.measure_toMeasurable`
`measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop` 📖	mathematical	`MeasurableSet` `IsCompact` `closure`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `addHaarScalarFactor`	—	`le_antisymm` `IsScalarTower.right` `exists_continuous_one_zero_of_isCompact` `IsTopologicalAddGroup.regularSpace` `isClosed_empty` `Set.disjoint_empty` `IsClosed.preimage` `isClosed_singleton` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `HasCompactSupport.isCompact_preimage` `Set.mem_singleton_iff` `zero_ne_one` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsClosed.closure_subset_iff` `smul_measure_isAddInvariant_le_of_isCompact_closure` `MeasurableSet.diff` `IsClosed.measurableSet` `BorelSpace.opensMeasurable` `IsCompact.closure_of_subset` `instR1Space` `Set.diff_subset` `measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport` `ENNReal.sub_le_sub_iff_left` `MeasureTheory.measure_mono` `instOuterMeasureClass` `LT.lt.ne` `IsCompact.measure_lt_top` `MeasureTheory.measure_diff` `MeasurableSet.nullMeasurableSet` `LE.le.trans_lt` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts`
`measure_isAddInvariant_eq_smul_of_isCompact_closure_of_measurableSet` 📖	mathematical	`MeasurableSet` `IsCompact` `closure`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `addHaarScalarFactor`	—	`isAddHaarMeasure_addHaarMeasure` `measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop` `Regular.instInnerRegularCompactLTTop` `regular_addHaarMeasure` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `IsAddHaarMeasure.toIsAddLeftInvariant` `smul_smul` `addHaarScalarFactor_eq_mul`
`measure_isAddLeftInvariant_eq_vadd_of_ne_top` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `addHaarScalarFactor`	—	`IsScalarTower.right` `ENNReal.mul_eq_top` `ENNReal.coe_eq_zero` `LT.lt.ne` `ENNReal.coe_ne_top` `MeasurableSet.measure_eq_iSup_isCompact_of_ne_top` `InnerRegularCompactLTTop.smul_nnreal` `iSup_congr_Prop` `measure_isAddInvariant_eq_smul_of_isCompact_closure` `IsCompact.closure` `instR1Space` `IsTopologicalAddGroup.regularSpace` `Set.subset_inter` `MeasureTheory.subset_toMeasurable` `le_antisymm` `LE.le.trans` `MeasureTheory.measure_mono` `instOuterMeasureClass` `Set.inter_subset_left` `Eq.le` `MeasureTheory.measure_toMeasurable` `Set.inter_subset_right` `MeasurableSet.inter` `MeasureTheory.measurableSet_toMeasurable` `LE.le.trans_lt` `Ne.lt_top`
`measure_isHaarMeasure_eq_smul_of_isEverywherePos` 📖	mathematical	`MeasurableSet` `IsEverywherePos`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `haarScalarFactor` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `IsHaarMeasure.toIsMulLeftInvariant`	—	`IsScalarTower.right` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `IsHaarMeasure.toIsMulLeftInvariant` `WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `IsCompact.closure` `instR1Space` `IsTopologicalGroup.regularSpace` `isClosed_closure` `Filter.mem_of_superset` `subset_closure` `mem_of_mem_nhds` `zorn_subset` `IsChain.directedOn` `Set.instReflSubset` `Set.subset_biUnion_of_mem` `Maximal.prop` `Maximal.mem_of_prop_insert` `Set.union_singleton` `inv_one` `mul_one` `mem_leftCoset` `Set.mul_mem_mul` `Set.inv_mem_inv` `Set.mem_biUnion` `mul_zpow_neg_one` `neg_neg` `zpow_one` `Mathlib.Tactic.Group.zpow_trick_one` `neg_add_cancel` `zpow_zero` `add_neg_cancel` `one_mul` `mem_leftCoset_iff` `Set.eq_empty_or_nonempty` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `MeasureTheory.measure_empty` `instOuterMeasureClass` `Set.Countable.exists_eq_range` `MeasurableSet.disjointed` `MeasurableSet.inter` `IsClosed.smul_left_of_isCompact` `IsTopologicalGroup.toContinuousInv` `ContinuousMul.to_continuousSMul` `IsTopologicalGroup.toContinuousMul` `IsClosed.inv` `IsClosed.measurableSet` `BorelSpace.opensMeasurable` `IsClosed.smul` `IsScalarTower.continuousConstSMul` `IsScalarTower.left` `Set.inter_iUnion` `Set.inter_eq_left` `Set.iUnion_exists` `Set.iUnion_iUnion_eq'` `MeasureTheory.measure_iUnion` `instCountableNat` `disjoint_disjointed` `iUnion_disjointed` `measure_isMulInvariant_eq_smul_of_isCompact_closure` `IsCompact.smul` `IsCompact.mul` `IsCompact.inv` `IsCompact.closure_of_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `disjointed_subset` `Set.inter_subset_right` `Mathlib.Tactic.Contrapose.contrapose₂` `lt_of_le_of_lt` `MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint` `Set.PairwiseDisjoint.mono` `Set.Pairwise.on_injective` `Subtype.val_injective` `MeasureTheory.measure_mono` `Set.iUnion_coe_set` `Ne.lt_top` `Summable.countable_support_ennreal` `LT.lt.ne` `Set.eq_univ_iff_forall` `ne_of_gt` `inter_mem_nhdsWithin` `Set.countable_univ_iff` `Set.to_countable` `IsEverywherePos.smul_measure_nnreal` `LT.lt.ne'` `haarScalarFactor_pos_of_isHaarMeasure` `IsEverywherePos.of_forall_exists_nhds_eq`
`measure_isHaarMeasure_eq_smul_of_isOpen` 📖	mathematical	`IsOpen`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `haarScalarFactor` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `IsHaarMeasure.toIsMulLeftInvariant`	—	`measure_isHaarMeasure_eq_smul_of_isEverywherePos` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `IsOpen.isEverywherePos` `IsHaarMeasure.toIsOpenPosMeasure`
`measure_isMulInvariant_eq_smul_of_isCompact_closure` 📖	mathematical	`IsCompact` `closure`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `haarScalarFactor`	—	`IsScalarTower.right` `le_antisymm` `MeasureTheory.measure_mono` `instOuterMeasureClass` `Set.subset_inter` `MeasureTheory.subset_toMeasurable` `subset_closure` `measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet` `MeasurableSet.inter` `MeasureTheory.measurableSet_toMeasurable` `IsClosed.measurableSet` `BorelSpace.opensMeasurable` `isClosed_closure` `IsCompact.closure_of_subset` `instR1Space` `IsTopologicalGroup.regularSpace` `Set.inter_subset_right` `Set.inter_subset_left` `MeasureTheory.measure_toMeasurable`
`measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop` 📖	mathematical	`MeasurableSet` `IsCompact` `closure`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `haarScalarFactor`	—	`le_antisymm` `IsScalarTower.right` `exists_continuous_one_zero_of_isCompact` `IsTopologicalGroup.regularSpace` `isClosed_empty` `Set.disjoint_empty` `IsClosed.preimage` `isClosed_singleton` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `HasCompactSupport.isCompact_preimage` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsClosed.closure_subset_iff` `smul_measure_isMulInvariant_le_of_isCompact_closure` `MeasurableSet.diff` `IsClosed.measurableSet` `BorelSpace.opensMeasurable` `IsCompact.closure_of_subset` `instR1Space` `Set.diff_subset` `measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport` `ENNReal.sub_le_sub_iff_left` `MeasureTheory.measure_mono` `instOuterMeasureClass` `LT.lt.ne` `IsCompact.measure_lt_top` `MeasureTheory.measure_diff` `MeasurableSet.nullMeasurableSet` `LE.le.trans_lt` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `IsHaarMeasure.toIsFiniteMeasureOnCompacts`
`measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet` 📖	mathematical	`MeasurableSet` `IsCompact` `closure`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `haarScalarFactor`	—	`isHaarMeasure_haarMeasure` `measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop` `Regular.instInnerRegularCompactLTTop` `regular_haarMeasure` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `IsHaarMeasure.toIsMulLeftInvariant` `smul_smul` `haarScalarFactor_eq_mul`
`measure_isMulLeftInvariant_eq_smul_of_ne_top` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `haarScalarFactor`	—	`IsScalarTower.right` `LT.lt.ne` `MeasurableSet.measure_eq_iSup_isCompact_of_ne_top` `InnerRegularCompactLTTop.smul_nnreal` `iSup_congr_Prop` `measure_isMulInvariant_eq_smul_of_isCompact_closure` `IsCompact.closure` `instR1Space` `IsTopologicalGroup.regularSpace` `Set.subset_inter` `MeasureTheory.subset_toMeasurable` `le_antisymm` `LE.le.trans` `MeasureTheory.measure_mono` `instOuterMeasureClass` `Set.inter_subset_left` `Eq.le` `MeasureTheory.measure_toMeasurable` `Set.inter_subset_right` `MeasurableSet.inter` `MeasureTheory.measurableSet_toMeasurable` `LE.le.trans_lt` `Ne.lt_top`
`measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasCompactSupport` `Real.instZero`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.preimage` `Set.instSingletonSet` `Real.instOne` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `addHaarScalarFactor`	—	`exists_seq_strictAnti_tendsto'` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Continuous.comp` `continuous_induced_dom` `BoundedContinuousFunction.continuous` `MeasureTheory.tendsto_integral_of_dominated_convergence` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `MeasureTheory.IntegrableOn.integrable_indicator` `MeasureTheory.integrableOn_const_iff` `enorm_one` `NormedDivisionRing.to_normOneClass` `ENNReal.one_ne_top` `one_ne_zero` `ENNReal.instCharZero` `IsCompact.measure_lt_top` `IsClosed.measurableSet` `isClosed_tsupport` `Filter.Eventually.of_forall` `instOuterMeasureClass` `NNReal.abs_eq` `Set.indicator_of_mem` `thickenedIndicator.congr_simp` `Nat.cast_one` `NNReal.coe_le_coe` `thickenedIndicator_le_one` `Set.indicator_of_notMem` `thickenedIndicator_zero` `Metric.thickening_singleton` `image_eq_zero_of_notMem_tsupport` `Metric.mem_ball` `dist_zero` `CStarRing.norm_of_mem_unitary` `instCStarRingReal` `Real.instNontrivial` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `not_lt` `LT.lt.le` `le_refl` `Filter.univ_mem'` `tendsto_pi_nhds` `thickenedIndicator_tendsto_indicator_closure` `Set.indicator_singleton` `NNReal.coe_single` `NNReal.tendsto_coe` `closure_singleton` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `IsScalarTower.right` `integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport` `HasCompactSupport.comp_left` `NNReal.coe_eq_zero` `thickenedIndicatorAux_zero` `tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `Set.indicator_comp_right` `IsClosed.preimage` `isClosed_singleton` `MeasureTheory.integral_indicator_const` `Real.instCompleteSpace` `mul_one` `HasCompactSupport.isCompact_preimage` `Set.mem_singleton_iff` `zero_ne_one` `MeasureTheory.measureReal_eq_measureReal_iff` `LT.lt.ne`
`measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasCompactSupport` `Real.instZero`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.preimage` `Set.instSingletonSet` `Real.instOne` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `haarScalarFactor`	—	`exists_seq_strictAnti_tendsto'` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Continuous.comp` `continuous_induced_dom` `BoundedContinuousFunction.continuous` `MeasureTheory.tendsto_integral_of_dominated_convergence` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `MeasureTheory.IntegrableOn.integrable_indicator` `enorm_one` `NormedDivisionRing.to_normOneClass` `ENNReal.instCharZero` `IsCompact.measure_lt_top` `IsClosed.measurableSet` `isClosed_tsupport` `Filter.Eventually.of_forall` `instOuterMeasureClass` `NNReal.abs_eq` `Set.indicator_of_mem` `thickenedIndicator.congr_simp` `Nat.cast_one` `thickenedIndicator_le_one` `Set.indicator_of_notMem` `thickenedIndicator_zero` `Metric.thickening_singleton` `image_eq_zero_of_notMem_tsupport` `dist_zero` `CStarRing.norm_of_mem_unitary` `instCStarRingReal` `Real.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `LT.lt.le` `Filter.univ_mem'` `tendsto_pi_nhds` `thickenedIndicator_tendsto_indicator_closure` `Set.indicator_singleton` `NNReal.coe_single` `NNReal.tendsto_coe` `closure_singleton` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `IsScalarTower.right` `integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport` `HasCompactSupport.comp_left` `thickenedIndicatorAux_zero` `tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `Set.indicator_comp_right` `IsClosed.preimage` `isClosed_singleton` `MeasureTheory.integral_indicator_const` `Real.instCompleteSpace` `mul_one` `HasCompactSupport.isCompact_preimage` `MeasureTheory.measureReal_eq_measureReal_iff` `LT.lt.ne`
`mul_addHaarScalarFactor_smul` 📖	mathematical	—	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `addHaarScalarFactor` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `IsAddHaarMeasure.nnreal_smul`	—	`IsScalarTower.right` `IsAddHaarMeasure.nnreal_smul` `exists_continuous_nonneg_pos` `IsTopologicalAddGroup.regularSpace` `ne_of_gt` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `BorelSpace.opensMeasurable` `IsAddHaarMeasure.toIsOpenPosMeasure` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `NNReal.coe_injective` `addHaarScalarFactor_eq_integral_div` `MeasureTheory.integral_smul_nnreal_measure` `IsUnit.smul_eq_zero` `isUnit_iff_ne_zero` `NNReal.smul_def` `smul_eq_mul` `mul_div_assoc` `mul_div_mul_left` `NNReal.coe_eq_zero`
`mul_haarScalarFactor_smul` 📖	mathematical	—	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `haarScalarFactor` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `IsHaarMeasure.nnreal_smul`	—	`IsScalarTower.right` `IsHaarMeasure.nnreal_smul` `exists_continuous_nonneg_pos` `IsTopologicalGroup.regularSpace` `ne_of_gt` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `BorelSpace.opensMeasurable` `IsHaarMeasure.toIsOpenPosMeasure` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `NNReal.coe_injective` `haarScalarFactor_eq_integral_div` `MeasureTheory.integral_smul_nnreal_measure` `NNReal.smul_def` `smul_eq_mul` `mul_div_assoc` `mul_div_mul_left`
`smul_measure_isAddInvariant_le_of_isCompact_closure` 📖	mathematical	`MeasurableSet` `IsCompact` `closure`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `addHaarScalarFactor` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike`	—	`le_of_forall_lt` `IsScalarTower.right` `LT.lt.ne` `LE.le.trans_lt` `MeasureTheory.measure_mono` `instOuterMeasureClass` `subset_closure` `IsCompact.measure_lt_top` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup` `MeasureTheory.isAddLeftInvariant_smul_nnreal` `IsAddHaarMeasure.toIsAddLeftInvariant` `InnerRegularCompactLTTop.smul_nnreal` `measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport`
`smul_measure_isMulInvariant_le_of_isCompact_closure` 📖	mathematical	`MeasurableSet` `IsCompact` `closure`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `NNReal` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `haarScalarFactor` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike`	—	`le_of_forall_lt` `IsScalarTower.right` `LT.lt.ne` `LE.le.trans_lt` `MeasureTheory.measure_mono` `instOuterMeasureClass` `subset_closure` `IsCompact.measure_lt_top` `MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group` `MeasureTheory.isMulLeftInvariant_smul_nnreal` `IsHaarMeasure.toIsMulLeftInvariant` `InnerRegularCompactLTTop.smul_nnreal` `measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport`

MeasureTheory.Measure.IsAddHaarMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNegInvariant_of_innerRegular` 📖	mathematical	—	`MeasureTheory.Measure.IsNegInvariant` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`MeasureTheory.Measure.IsFiniteMeasureOnCompacts.neg` `IsTopologicalAddGroup.toContinuousNeg` `toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.neg.instIsAddLeftInvariant` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousNeg.measurableNeg` `MeasureTheory.IsAddLeftInvariant.isAddRightInvariant` `toIsAddLeftInvariant` `IsScalarTower.right` `MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_innerRegular` `MeasureTheory.Measure.InnerRegular.neg` `MeasureTheory.Measure.neg_def` `MeasureTheory.Measure.map_smul` `smul_smul` `pow_two` `Function.Involutive.comp_self` `neg_involutive` `MeasureTheory.Measure.map_id` `MeasureTheory.Measure.map_map` `Continuous.measurable` `BorelSpace.opensMeasurable` `ContinuousNeg.continuous_neg` `TopologicalSpace.PositiveCompacts.nonempty'` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `Zero.instNonempty` `one_pow` `one_mul` `LT.lt.ne'` `MeasureTheory.Measure.measure_pos_of_nonempty_interior` `toIsOpenPosMeasure` `TopologicalSpace.PositiveCompacts.interior_nonempty` `LT.lt.ne` `IsCompact.measure_lt_top` `TopologicalSpace.PositiveCompacts.isCompact` `StrictMono.injective` `ENNReal.pow_right_strictMono` `two_ne_zero` `one_smul`
`isNegInvariant_of_regular` 📖	mathematical	—	`MeasureTheory.Measure.IsNegInvariant` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`MeasureTheory.Measure.IsFiniteMeasureOnCompacts.neg` `IsTopologicalAddGroup.toContinuousNeg` `toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.neg.instIsAddLeftInvariant` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousNeg.measurableNeg` `MeasureTheory.IsAddLeftInvariant.isAddRightInvariant` `toIsAddLeftInvariant` `IsScalarTower.right` `MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_regular` `MeasureTheory.Measure.Regular.neg` `MeasureTheory.Measure.neg_def` `MeasureTheory.Measure.map_smul` `smul_smul` `pow_two` `Function.Involutive.comp_self` `neg_involutive` `MeasureTheory.Measure.map_id` `MeasureTheory.Measure.map_map` `Continuous.measurable` `BorelSpace.opensMeasurable` `ContinuousNeg.continuous_neg` `TopologicalSpace.PositiveCompacts.nonempty'` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `Zero.instNonempty` `one_pow` `one_mul` `LT.lt.ne'` `MeasureTheory.Measure.measure_pos_of_nonempty_interior` `toIsOpenPosMeasure` `TopologicalSpace.PositiveCompacts.interior_nonempty` `LT.lt.ne` `IsCompact.measure_lt_top` `TopologicalSpace.PositiveCompacts.isCompact` `StrictMono.injective` `ENNReal.pow_right_strictMono` `two_ne_zero` `one_smul`

MeasureTheory.Measure.IsHaarMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isInvInvariant_of_innerRegular` 📖	mathematical	—	`MeasureTheory.Measure.IsInvInvariant` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`MeasureTheory.Measure.IsFiniteMeasureOnCompacts.inv` `IsTopologicalGroup.toContinuousInv` `toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.inv.instIsMulLeftInvariant` `ContinuousMul.measurableMul` `IsTopologicalGroup.toContinuousMul` `ContinuousInv.measurableInv` `MeasureTheory.IsMulLeftInvariant.isMulRightInvariant` `toIsMulLeftInvariant` `IsScalarTower.right` `MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegular` `MeasureTheory.Measure.InnerRegular.inv` `MeasureTheory.Measure.inv_def` `MeasureTheory.Measure.map_smul` `smul_smul` `pow_two` `Function.Involutive.comp_self` `MeasureTheory.Measure.map_id` `MeasureTheory.Measure.map_map` `Continuous.measurable` `BorelSpace.opensMeasurable` `ContinuousInv.continuous_inv` `TopologicalSpace.PositiveCompacts.nonempty'` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `One.instNonempty` `one_pow` `one_mul` `LT.lt.ne'` `MeasureTheory.Measure.measure_pos_of_nonempty_interior` `toIsOpenPosMeasure` `TopologicalSpace.PositiveCompacts.interior_nonempty` `LT.lt.ne` `IsCompact.measure_lt_top` `TopologicalSpace.PositiveCompacts.isCompact` `StrictMono.injective` `ENNReal.pow_right_strictMono` `two_ne_zero` `one_smul`
`isInvInvariant_of_regular` 📖	mathematical	—	`MeasureTheory.Measure.IsInvInvariant` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`MeasureTheory.Measure.IsFiniteMeasureOnCompacts.inv` `IsTopologicalGroup.toContinuousInv` `toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.inv.instIsMulLeftInvariant` `ContinuousMul.measurableMul` `IsTopologicalGroup.toContinuousMul` `ContinuousInv.measurableInv` `MeasureTheory.IsMulLeftInvariant.isMulRightInvariant` `toIsMulLeftInvariant` `IsScalarTower.right` `MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular` `MeasureTheory.Measure.Regular.inv` `MeasureTheory.Measure.inv_def` `MeasureTheory.Measure.map_smul` `smul_smul` `pow_two` `Function.Involutive.comp_self` `MeasureTheory.Measure.map_id` `MeasureTheory.Measure.map_map` `Continuous.measurable` `BorelSpace.opensMeasurable` `ContinuousInv.continuous_inv` `TopologicalSpace.PositiveCompacts.nonempty'` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `One.instNonempty` `one_pow` `one_mul` `LT.lt.ne'` `MeasureTheory.Measure.measure_pos_of_nonempty_interior` `toIsOpenPosMeasure` `TopologicalSpace.PositiveCompacts.interior_nonempty` `LT.lt.ne` `IsCompact.measure_lt_top` `TopologicalSpace.PositiveCompacts.isCompact` `StrictMono.injective` `ENNReal.pow_right_strictMono` `two_ne_zero` `one_smul`

MeasureTheory.Measure.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zpow` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`MeasureTheory.MeasurePreserving.comp` `MeasureTheory.Measure.measurePreserving_zpow`
`zsmul` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`MeasureTheory.MeasurePreserving.comp` `MeasureTheory.Measure.measurePreserving_zsmul`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurePreserving` 📖	mathematical	`Continuous` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.univ`	`MeasureTheory.MeasurePreserving`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `MeasureTheory.measure_lt_top` `MeasureTheory.CompactSpace.isFiniteMeasure` `MeasureTheory.Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.isHaarMeasure_map_of_isFiniteMeasure` `IsTopologicalGroup.toContinuousMul` `MeasureTheory.Measure.IsHaarMeasure.toIsMulLeftInvariant` `IsScalarTower.right` `MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegular` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `IsTopologicalGroup.regularSpace` `instWeaklyLocallyCompactSpaceOfCompactSpace` `MeasureTheory.Measure.instInnerRegularOfIsHaarMeasureOfCompactSpace` `one_mul` `smul_eq_mul` `ENNReal.smul_def` `MeasureTheory.Measure.smul_apply` `MeasureTheory.Measure.map_apply` `MeasurableSet.univ` `Set.preimage_univ` `ENNReal.coe_eq_one` `MeasureTheory.Measure.instNeZeroENNRealCoeSetUniv` `MeasureTheory.Measure.instNeZeroOfNonempty` `MeasureTheory.Measure.IsHaarMeasure.toIsOpenPosMeasure` `One.instNonempty` `MeasureTheory.measure_ne_top` `one_smul`

---

← Back to Index