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_integral_div_of_continuous_nonneg_pos, addHaarScalarFactor_eq_mul, addHaarScalarFactor_map, 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_integral_div_of_continuous_nonneg_pos, haarScalarFactor_eq_mul, haarScalarFactor_map, 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	71
Total	73

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 DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLike	—	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	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup integral AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid 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	32 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, addHaarScalarFactor_map, 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_eq_integral_div_of_continuous_nonneg_pos, addHaarScalarFactor_pos_of_isAddHaarMeasure, isAddLeftInvariant_eq_smul, addHaarScalarFactor_smul, euclideanHausdorffMeasure_def, addHaarScalarFactor_self
haarScalarFactor 📖	CompOp	24 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, haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos, mul_haarScalarFactor_smul, haarScalarFactor_eq_mul, haarScalarFactor_map, 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 Real 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_integral_div_of_continuous_nonneg_pos 📖	mathematical	HasCompactSupport Real Real.instZero DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Preorder.toLE PartialOrder.toPreorder ContinuousMap.partialOrder Real.partialOrder ContinuousMap.instZero	NNReal.toReal addHaarScalarFactor Real DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike	—	ne_of_gt Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero BorelSpace.opensMeasurable IsAddHaarMeasure.toIsOpenPosMeasure IsAddHaarMeasure.toIsFiniteMeasureOnCompacts ContinuousMap.continuous_toFun addHaarScalarFactor_eq_integral_div
addHaarScalarFactor_eq_mul 📖	mathematical	—	addHaarScalarFactor NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring 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_map 📖	mathematical	—	addHaarScalarFactor map DFunLike.coe ContinuousAddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike ContinuousAddEquiv.instEquivLike ContinuousAddEquiv.isAddHaarMeasure_map IsAddHaarMeasure.toIsFiniteMeasureOnCompacts IsAddHaarMeasure.toIsAddLeftInvariant	—	ContinuousAddEquiv.isAddHaarMeasure_map IsAddHaarMeasure.toIsFiniteMeasureOnCompacts IsAddHaarMeasure.toIsAddLeftInvariant exists_continuous_nonneg_pos IsTopologicalAddGroup.regularSpace ne_of_gt Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero BorelSpace.opensMeasurable IsAddHaarMeasure.toIsOpenPosMeasure addHaarScalarFactor_eq_integral_div_of_continuous_nonneg_pos addHaarScalarFactor_eq_integral_div Continuous.comp Homeomorph.continuous HasCompactSupport.comp_homeomorph MeasureTheory.integral_map Continuous.aemeasurable ContinuousMapClass.map_continuous HomeomorphClass.instContinuousMapClass ContinuousAddEquiv.instHomeomorphClass Continuous.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal ContinuousMap.instContinuousMapClass exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport
addHaarScalarFactor_pos_of_isAddHaarMeasure 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero addHaarScalarFactor IsAddHaarMeasure.toIsFiniteMeasureOnCompacts IsAddHaarMeasure.toIsAddLeftInvariant	—	IsAddHaarMeasure.toIsFiniteMeasureOnCompacts IsAddHaarMeasure.toIsAddLeftInvariant pos_iff_ne_zero addHaarScalarFactor_self MulZeroClass.zero_mul one_ne_zero NeZero.charZero_one IsStrictOrderedRing.toCharZero addHaarScalarFactor_eq_mul
addHaarScalarFactor_self 📖	mathematical	—	addHaarScalarFactor IsAddHaarMeasure.toIsFiniteMeasureOnCompacts IsAddHaarMeasure.toIsAddLeftInvariant NNReal NNReal.instOne	—	IsAddHaarMeasure.toIsFiniteMeasureOnCompacts IsAddHaarMeasure.toIsAddLeftInvariant exists_continuous_nonneg_pos IsTopologicalAddGroup.regularSpace ne_of_gt Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero BorelSpace.opensMeasurable IsAddHaarMeasure.toIsOpenPosMeasure ContinuousMap.continuous_toFun NNReal.coe_injective addHaarScalarFactor_eq_integral_div_of_continuous_nonneg_pos div_self exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport
addHaarScalarFactor_smul 📖	mathematical	—	addHaarScalarFactor NNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring 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 NNReal.coe_injective addHaarScalarFactor_eq_integral_div_of_continuous_nonneg_pos 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 NNReal.instCommSemiring 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	—	NNReal MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring 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 instSeparatelyContinuousAddOfContinuousAdd 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
exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport 📖	mathematical	—	NNReal MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring 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 instSeparatelyContinuousMulOfContinuousMul 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
haarScalarFactor_eq_integral_div 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace HasCompactSupport Real.instZero	NNReal.toReal haarScalarFactor Real 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_integral_div_of_continuous_nonneg_pos 📖	mathematical	HasCompactSupport Real Real.instZero DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Preorder.toLE PartialOrder.toPreorder ContinuousMap.partialOrder Real.partialOrder ContinuousMap.instZero	NNReal.toReal haarScalarFactor Real DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike	—	ne_of_gt Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero BorelSpace.opensMeasurable IsHaarMeasure.toIsOpenPosMeasure IsHaarMeasure.toIsFiniteMeasureOnCompacts ContinuousMap.continuous_toFun haarScalarFactor_eq_integral_div
haarScalarFactor_eq_mul 📖	mathematical	—	haarScalarFactor NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring 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_map 📖	mathematical	—	haarScalarFactor map DFunLike.coe ContinuousMulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike ContinuousMulEquiv.instEquivLike ContinuousMulEquiv.isHaarMeasure_map IsHaarMeasure.toIsFiniteMeasureOnCompacts IsHaarMeasure.toIsMulLeftInvariant	—	ContinuousMulEquiv.isHaarMeasure_map IsHaarMeasure.toIsFiniteMeasureOnCompacts IsHaarMeasure.toIsMulLeftInvariant exists_continuous_nonneg_pos IsTopologicalGroup.regularSpace ne_of_gt Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero BorelSpace.opensMeasurable IsHaarMeasure.toIsOpenPosMeasure haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos haarScalarFactor_eq_integral_div Continuous.comp Homeomorph.continuous HasCompactSupport.comp_homeomorph MeasureTheory.integral_map Continuous.aemeasurable ContinuousMapClass.map_continuous HomeomorphClass.instContinuousMapClass ContinuousMulEquiv.instHomeomorphClass Continuous.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal ContinuousMap.instContinuousMapClass exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport
haarScalarFactor_pos_of_isHaarMeasure 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero haarScalarFactor IsHaarMeasure.toIsFiniteMeasureOnCompacts IsHaarMeasure.toIsMulLeftInvariant	—	IsHaarMeasure.toIsFiniteMeasureOnCompacts IsHaarMeasure.toIsMulLeftInvariant pos_iff_ne_zero haarScalarFactor_self MulZeroClass.zero_mul NeZero.charZero_one IsStrictOrderedRing.toCharZero haarScalarFactor_eq_mul
haarScalarFactor_self 📖	mathematical	—	haarScalarFactor IsHaarMeasure.toIsFiniteMeasureOnCompacts IsHaarMeasure.toIsMulLeftInvariant NNReal NNReal.instOne	—	IsHaarMeasure.toIsFiniteMeasureOnCompacts IsHaarMeasure.toIsMulLeftInvariant exists_continuous_nonneg_pos IsTopologicalGroup.regularSpace ne_of_gt Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero BorelSpace.opensMeasurable IsHaarMeasure.toIsOpenPosMeasure ContinuousMap.continuous_toFun NNReal.coe_injective haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos div_self exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport
haarScalarFactor_smul 📖	mathematical	—	haarScalarFactor NNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring 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 NNReal.coe_injective haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos MeasureTheory.integral_smul_nnreal_measure smul_div_assoc
haarScalarFactor_smul_smul 📖	mathematical	—	haarScalarFactor NNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring 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 Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal NNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring 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 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.add_const instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd 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 Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal NNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring 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 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.mul_const instSeparatelyContinuousMulOfContinuousMul IsTopologicalGroup.toContinuousMul 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 OuterRegular.ext_isOpen WeaklyRegular.toOuterRegular Regular.weaklyRegular instR1Space IsTopologicalAddGroup.regularSpace OuterRegular.smul_nnreal
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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 OuterRegular.ext_isOpen WeaklyRegular.toOuterRegular Regular.weaklyRegular instR1Space IsTopologicalGroup.regularSpace OuterRegular.smul_nnreal
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 NNReal.instCommSemiring 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 SeparatelyContinuousAdd.to_continuousVAdd instSeparatelyContinuousAddOfContinuousAdd 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 SeparatelyContinuousMul.to_continuousSMul instSeparatelyContinuousMulOfContinuousMul 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 Real Set.instSingletonSet Real.instOne NNReal Algebra.toSMul NNReal.instCommSemiring 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 instReflLe 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 Real Set.instSingletonSet Real.instOne NNReal Algebra.toSMul NNReal.instCommSemiring 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 instReflLe 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 NNReal.instSemiring addHaarScalarFactor MeasureTheory.Measure instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right IsAddHaarMeasure.nnreal_smul	—	IsScalarTower.right IsAddHaarMeasure.nnreal_smul exists_continuous_nonneg_pos IsTopologicalAddGroup.regularSpace NNReal.coe_injective addHaarScalarFactor_eq_integral_div_of_continuous_nonneg_pos MeasureTheory.integral_smul_nnreal_measure 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 NNReal.instSemiring haarScalarFactor MeasureTheory.Measure instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right IsHaarMeasure.nnreal_smul	—	IsScalarTower.right IsHaarMeasure.nnreal_smul exists_continuous_nonneg_pos IsTopologicalGroup.regularSpace NNReal.coe_injective haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos 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 NNReal.instCommSemiring 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 NNReal.instCommSemiring 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 instSeparatelyContinuousAddOfContinuousAdd 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 instSeparatelyContinuousAddOfContinuousAdd 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 instSeparatelyContinuousMulOfContinuousMul 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 instSeparatelyContinuousMulOfContinuousMul 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	MeasureTheory.MeasurePreserving DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	MeasureTheory.MeasurePreserving.comp MeasureTheory.Measure.measurePreserving_zpow
zsmul 📖	mathematical	MeasureTheory.MeasurePreserving	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 DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLike	—	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