DistribChar

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

Statistics

Metric	Count
Definitions distribHaarChar	1
Theorems addHaarScalarFactor_smul_eq_distribHaarChar, addHaarScalarFactor_smul_eq_distribHaarChar_inv, addHaarScalarFactor_smul_inv_eq_distribHaarChar, distribHaarChar_apply, distribHaarChar_eq_div, distribHaarChar_eq_of_measure_smul_eq_mul, distribHaarChar_mul, distribHaarChar_pos	8
Total	9

MeasureTheory

Definitions

Name	Category	Theorems
distribHaarChar 📖	CompOp	8 math math: addHaarScalarFactor_smul_inv_eq_distribHaarChar, addHaarScalarFactor_smul_eq_distribHaarChar_inv, addHaarScalarFactor_smul_eq_distribHaarChar, distribHaarChar_apply, distribHaarChar_eq_of_measure_smul_eq_mul, distribHaarChar_eq_div, distribHaarChar_mul, distribHaarChar_pos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addHaarScalarFactor_smul_eq_distribHaarChar 📖	mathematical	—	Measure.addHaarScalarFactor AddCommGroup.toAddGroup DomMulAct Measure SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Measure.instAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DomMulAct.instMonoidOfMulOpposite MulOpposite.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.instDistribMulActionDomMulAct DistribMulAction.toMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid ContinuousConstSMul.toMeasurableConstSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsAddHaarMeasure.domSMul Measure.IsAddHaarMeasure.toIsAddLeftInvariant MonoidHom NNReal MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidHom.instFunLike distribHaarChar	—	BorelSpace.measurable_eq ContinuousConstSMul.toMeasurableConstSMul Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsAddHaarMeasure.domSMul Measure.IsAddHaarMeasure.toIsAddLeftInvariant Measure.addHaarScalarFactor_smul_congr' Measure.isAddHaarMeasure_addHaarMeasure
addHaarScalarFactor_smul_eq_distribHaarChar_inv 📖	mathematical	—	Measure.addHaarScalarFactor AddCommGroup.toAddGroup DomMulAct Measure SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Measure.instAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DomMulAct.instMonoidOfMulOpposite MulOpposite.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.instDistribMulActionDomMulAct DistribMulAction.toMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid ContinuousConstSMul.toMeasurableConstSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Measure.IsAddHaarMeasure.domSMul Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsAddHaarMeasure.toIsAddLeftInvariant NNReal NNReal.instInv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidHom.instFunLike distribHaarChar	—	ContinuousConstSMul.toMeasurableConstSMul Measure.IsAddHaarMeasure.domSMul Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsAddHaarMeasure.toIsAddLeftInvariant map_inv MonoidHom.instMonoidHomClass addHaarScalarFactor_smul_inv_eq_distribHaarChar DomMulAct.mk_inv inv_inv
addHaarScalarFactor_smul_inv_eq_distribHaarChar 📖	mathematical	—	Measure.addHaarScalarFactor AddCommGroup.toAddGroup DomMulAct Measure SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Measure.instAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DomMulAct.instMonoidOfMulOpposite MulOpposite.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.instDistribMulActionDomMulAct DistribMulAction.toMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid ContinuousConstSMul.toMeasurableConstSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DomMulAct.instInvOfMulOpposite MulOpposite.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Measure.IsAddHaarMeasure.domSMul Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsAddHaarMeasure.toIsAddLeftInvariant MonoidHom NNReal MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidHom.instFunLike distribHaarChar	—	ContinuousConstSMul.toMeasurableConstSMul Measure.IsAddHaarMeasure.domSMul Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsAddHaarMeasure.toIsAddLeftInvariant Measure.addHaarScalarFactor_domSMul Measure.addHaarScalarFactor.congr_simp mul_inv_cancel one_smul addHaarScalarFactor_smul_eq_distribHaarChar
distribHaarChar_apply 📖	mathematical	—	DFunLike.coe MonoidHom NNReal MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidHom.instFunLike distribHaarChar Measure.addHaarScalarFactor AddCommGroup.toAddGroup borel DomMulAct Measure SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Measure.instAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DomMulAct.instMonoidOfMulOpposite MulOpposite.instMonoid Measure.instDistribMulActionDomMulAct DistribMulAction.toMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Equiv EquivLike.toFunLike Equiv.instEquivLike Measure.addHaar	—	—
distribHaarChar_eq_div 📖	mathematical	—	ENNReal.ofNNReal DFunLike.coe MonoidHom NNReal MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidHom.instFunLike distribHaarChar ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid Measure Set Measure.instFunLike Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	distribHaarChar_mul ENNReal.mul_div_cancel_right
distribHaarChar_eq_of_measure_smul_eq_mul 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal	MonoidHom NNReal MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instSemiringNNReal MonoidHom.instFunLike distribHaarChar	—	ENNReal.coe_injective distribHaarChar_eq_div ENNReal.mul_div_cancel_right
distribHaarChar_mul 📖	mathematical	—	ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal DFunLike.coe MonoidHom NNReal MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instSemiringNNReal MonoidHom.instFunLike distribHaarChar Measure Set Measure.instFunLike Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	ContinuousConstSMul.toMeasurableConstSMul Measure.domSMul_apply Equiv.symm_apply_apply Measure.nnreal_smul_coe_apply Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsAddHaarMeasure.domSMul Measure.IsAddHaarMeasure.toIsAddLeftInvariant addHaarScalarFactor_smul_eq_distribHaarChar IsScalarTower.right Measure.smul_apply Measure.isAddLeftInvariant_eq_smul_of_regular Measure.Regular.domSMul
distribHaarChar_pos 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidHom.instFunLike distribHaarChar	—	pos_iff_ne_zero NNReal.instCanonicallyOrderedAdd IsUnit.ne_zero IsUnit.map MonoidHom.instMonoidHomClass Group.isUnit

---

← Back to Index