Arithmetic

📁 Source: Mathlib/MeasureTheory/Group/Arithmetic.lean

Statistics

Metric	Count
Definitions instMeasurableSpace, instMeasurableSpace, MeasurableAdd, MeasurableAdd₂, MeasurableConstSMul, MeasurableConstVAdd, MeasurableDiv, MeasurableDiv₂, MeasurableInv, MeasurableMul, MeasurableMul₂, MeasurableNeg, MeasurablePow, MeasurableSMul, MeasurableSMul₂, MeasurableSub, MeasurableSub₂, MeasurableVAdd, MeasurableVAdd₂, instMeasurableSpace, instMeasurableSpace	21
Theorems add, add', add_const, add_iff_left, add_iff_right, const_add, const_div, const_mul, const_pow, const_smul, const_sub, const_vadd, div, div', div_const, fun_const_smul, fun_const_vadd, inv, mul, mul', mul_const, mul_iff_left, mul_iff_right, neg, pow, pow_const, smul, smul_const, sub, sub', sub_const, vadd, vadd_const, measurableSMul_nat₂, instMeasurableAdd, instMeasurableConstVAdd, instMeasurableMul₂, instMeasurableConstVAdd, instMeasurableVAdd, instMeasurableConstVAdd, instMeasurableVAdd, instMeasurableConstVAdd, measurableVAdd, toMeasurableAdd, toMeasurableAdd₂, toMeasurableDiv, toMeasurableDiv₂, toMeasurableInv, toMeasurableMul, toMeasurableMul₂, toMeasurableNeg, toMeasurableSub, toMeasurableSub₂, measurableZPow, aemeasurable_fun_prod, aemeasurable_fun_sum, aemeasurable_prod, aemeasurable_sum, measurable_fun_prod, measurable_fun_sum, measurable_prod, measurable_prod_apply, measurable_sum, measurable_sum_apply, aemeasurable_const_vadd_iff, measurable_const_vadd_iff, aemeasurable_const_smul_iff, measurable_const_smul_iff, aemeasurable_fun_prod, aemeasurable_fun_sum, aemeasurable_prod, aemeasurable_sum, measurable_fun_prod, measurable_fun_sum, measurable_prod, measurable_sum, add, add', add_const, add_iff_left, add_iff_right, const_add, const_div, const_mul, const_pow, const_smul, const_sub, const_vadd, div, div', div_const, fun_const_smul, fun_const_vadd, inv, measurableSMul₂_iterateAddAct, measurableSMul₂_iterateMulAct, mul, mul', mul_const, mul_iff_left, mul_iff_right, neg, pow, pow_const, smul, smul', smul_const, sub, sub', sub_const, vadd, vadd', vadd_const, measurable_add_const, measurable_const_add, measurable_add, toMeasurableAdd, measurable_const_smul, measurable_const_vadd, measurable_const_div, measurable_div_const, toMeasurableInv, measurable_div, toMeasurableDiv, measurable_inv, measurable_const_mul, measurable_mul_const, measurable_mul, toMeasurableMul, measurable_neg, measurable_pow, measurable_smul_const, op, toMeasurableConstSMul, measurable_smul, op, toMeasurableSMul, inv, neg, measurable_const_sub, measurable_sub_const, measurable_sub, toMeasurableSub, measurable_vadd_const, op, toMeasurableConstVAdd, measurable_vadd, toMeasurableVAdd, measurablePow, instMeasurableConstSMul, instMeasurableMul, instMeasurableMul₂, aemeasurable_fun_prod, aemeasurable_fun_sum, aemeasurable_prod, aemeasurable_sum, measurable_fun_prod, measurable_fun_sum, measurable_prod, measurable_sum, instMeasurableConstSMul, instMeasurableConstVAdd, measurableAdd, measurableAdd₂, measurableDiv, measurableDiv₂, measurableInv, measurableMul, measurableMul₂, measurableNeg, measurableSMul, measurableSub, measurableSub₂, measurableVAdd, measurableSMul_int₂, instMeasurableConstSMul, instMeasurableSMul, instMeasurableConstSMul, instMeasurableSMul, instMeasurableConstSMul, measurableSMul, aemeasurable_const_smul_iff, aemeasurable_const_smul_iff₀, aemeasurable_const_vadd_iff, aemeasurable_inv_iff, aemeasurable_neg_iff, instMeasurableEqOfCanonicallyOrderedAddOfOrderedSubOfMeasurableSub₂OfMeasurableSingletonClass, instMeasurableEqOfMeasurableSingletonClassOfMeasurableSub₂, measurableDiv_of_mul_inv, measurableDiv₂_of_add_neg, measurableDiv₂_of_mul_inv, measurableEmbedding_inv, measurableEmbedding_neg, measurableSMul_iterateMulAct, measurableSMul_of_mul, measurableSMul_opposite_of_mul, measurableSMul₂_iterateAddAct, measurableSMul₂_iterateMulAct, measurableSMul₂_of_add, measurableSMul₂_of_mul, measurableSMul₂_opposite_of_add, measurableSMul₂_opposite_of_mul, measurableSet_eq_fun', measurableSet_eq_fun_of_countable, measurableSub_of_add_neg, measurableVAdd_iterateAddAct, measurableVAdd_of_add, measurableVAdd_opposite_of_add, measurable_add_op, measurable_add_unop, measurable_const_smul_iff, measurable_const_smul_iff₀, measurable_const_vadd_iff, measurable_div_const', measurable_inv_iff, measurable_mul_op, measurable_mul_unop, measurable_neg_iff, measurable_sub_const'	219
Total	240

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableAdd₂.measurable_add prodMk
add' 📖	mathematical	AEMeasurable	Pi.instAdd	—	Measurable.comp_aemeasurable MeasurableAdd₂.measurable_add prodMk
add_const 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableAdd.measurable_add_const
add_iff_left 📖	mathematical	AEMeasurable	Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	add_iff_right add_comm
add_iff_right 📖	mathematical	AEMeasurable	Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	add neg add_neg_cancel_comm
const_add 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableAdd.measurable_const_add
const_div 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableDiv.measurable_const_div
const_mul 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableMul.measurable_const_mul
const_pow 📖	—	AEMeasurable	—	—	pow aemeasurable_const
const_smul 📖	mathematical	AEMeasurable	Function.hasSMul	—	fun_const_smul
const_sub 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableSub.measurable_const_sub
const_vadd 📖	mathematical	AEMeasurable	HVAdd.hVAdd instHVAdd Function.hasVAdd	—	fun_const_vadd
div 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableDiv₂.measurable_div prodMk
div' 📖	mathematical	AEMeasurable	Pi.instDiv	—	Measurable.comp_aemeasurable MeasurableDiv₂.measurable_div prodMk
div_const 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableDiv.measurable_div_const
fun_const_smul 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableConstSMul.measurable_const_smul
fun_const_vadd 📖	mathematical	AEMeasurable	HVAdd.hVAdd instHVAdd	—	Measurable.comp_aemeasurable MeasurableConstVAdd.measurable_const_vadd
inv 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableInv.measurable_inv
mul 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableMul₂.measurable_mul prodMk
mul' 📖	mathematical	AEMeasurable	Pi.instMul	—	Measurable.comp_aemeasurable MeasurableMul₂.measurable_mul prodMk
mul_const 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableMul.measurable_mul_const
mul_iff_left 📖	mathematical	AEMeasurable	Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	mul_iff_right mul_comm
mul_iff_right 📖	mathematical	AEMeasurable	Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	mul inv mul_inv_cancel_comm
neg 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableNeg.measurable_neg
pow 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurablePow.measurable_pow prodMk
pow_const 📖	—	AEMeasurable	—	—	pow aemeasurable_const
smul 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableSMul₂.measurable_smul prodMk
smul_const 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable' Measurable.smul_const measurable_id'
sub 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableSub₂.measurable_sub prodMk
sub' 📖	mathematical	AEMeasurable	Pi.instSub	—	Measurable.comp_aemeasurable MeasurableSub₂.measurable_sub prodMk
sub_const 📖	—	AEMeasurable	—	—	Measurable.comp_aemeasurable MeasurableSub.measurable_sub_const
vadd 📖	mathematical	AEMeasurable	HVAdd.hVAdd instHVAdd	—	Measurable.comp_aemeasurable MeasurableVAdd₂.measurable_vadd prodMk
vadd_const 📖	mathematical	AEMeasurable	HVAdd.hVAdd instHVAdd	—	Measurable.comp_aemeasurable' Measurable.vadd_const measurable_id'

AddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSMul_nat₂ 📖	mathematical	—	MeasurableSMul₂ toNatSMul Nat.instMeasurableSpace	—	measurable_from_prod_countable_left instCountableNat Nat.instMeasurableSingletonClass zero_smul succ_nsmul Measurable.add measurable_id Measurable.comp measurable_swap

AddOpposite

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	7 math math: measurable_add_op, MeasurableVAdd.op, instMeasurableMul₂, instMeasurableAdd, measurableVAdd_opposite_of_add, measurable_add_unop, measurableSMul₂_opposite_of_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableAdd 📖	mathematical	—	MeasurableAdd AddOpposite instMeasurableSpace instAdd	—	Measurable.comp measurable_add_op Measurable.add_const measurable_add_unop Measurable.const_add
instMeasurableConstVAdd 📖	mathematical	—	MeasurableConstVAdd AddOpposite	—	forall IsCentralVAdd.op_vadd_eq_vadd MeasurableConstVAdd.measurable_const_vadd
instMeasurableMul₂ 📖	mathematical	—	MeasurableAdd₂ AddOpposite instMeasurableSpace instAdd	—	Measurable.comp measurable_add_op Measurable.add measurable_add_unop measurable_snd measurable_fst

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableConstVAdd 📖	mathematical	—	MeasurableConstVAdd AddSubgroup SetLike.instMembership instSetLike AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddAction.toAddSemigroupAction instAddAction	—	AddSubmonoid.instMeasurableConstVAdd
instMeasurableVAdd 📖	mathematical	—	MeasurableVAdd AddSubgroup SetLike.instMembership instSetLike AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddAction.toAddSemigroupAction instAddAction Subtype.instMeasurableSpace	—	AddSubmonoid.instMeasurableVAdd

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableConstVAdd 📖	mathematical	—	MeasurableConstVAdd AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership instSetLike vadd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	MeasurableConstVAdd.measurable_const_vadd
instMeasurableVAdd 📖	mathematical	—	MeasurableVAdd AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership instSetLike vadd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction Subtype.instMeasurableSpace	—	instMeasurableConstVAdd MeasurableVAdd.toMeasurableConstVAdd Measurable.comp MeasurableVAdd.measurable_vadd_const measurable_subtype_coe

AddUnits

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	1 math math: measurableVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableConstVAdd 📖	mathematical	—	MeasurableConstVAdd AddUnits instVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	MeasurableConstVAdd.measurable_const_vadd
measurableVAdd 📖	mathematical	—	MeasurableVAdd AddUnits instVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction instMeasurableSpace	—	instMeasurableConstVAdd MeasurableVAdd.toMeasurableConstVAdd Measurable.comp MeasurableVAdd.measurable_vadd_const MeasurableSpace.le_map_comap

DiscreteMeasurableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMeasurableAdd 📖	mathematical	—	MeasurableAdd	—	Measurable.of_discrete
toMeasurableAdd₂ 📖	mathematical	—	MeasurableAdd₂	—	Measurable.of_discrete
toMeasurableDiv 📖	mathematical	—	MeasurableDiv	—	Measurable.of_discrete
toMeasurableDiv₂ 📖	mathematical	—	MeasurableDiv₂	—	Measurable.of_discrete
toMeasurableInv 📖	mathematical	—	MeasurableInv	—	Measurable.of_discrete
toMeasurableMul 📖	mathematical	—	MeasurableMul	—	Measurable.of_discrete
toMeasurableMul₂ 📖	mathematical	—	MeasurableMul₂	—	Measurable.of_discrete
toMeasurableNeg 📖	mathematical	—	MeasurableNeg	—	Measurable.of_discrete
toMeasurableSub 📖	mathematical	—	MeasurableSub	—	Measurable.of_discrete
toMeasurableSub₂ 📖	mathematical	—	MeasurableSub₂	—	Measurable.of_discrete

DivInvMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableZPow 📖	mathematical	—	MeasurablePow Int.instMeasurableSpace toZPow	—	measurable_from_prod_countable_left instCountableInt Int.instMeasurableSingletonClass zpow_natCast Measurable.pow_const Monoid.measurablePow measurable_id zpow_negSucc Measurable.inv

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_fun_prod 📖	mathematical	AEMeasurable	prod	—	aemeasurable_prod
aemeasurable_fun_sum 📖	mathematical	AEMeasurable	sum	—	sum_apply aemeasurable_sum
aemeasurable_prod 📖	mathematical	AEMeasurable	prod Pi.commMonoid	—	Multiset.aemeasurable_prod Multiset.mem_map
aemeasurable_sum 📖	mathematical	AEMeasurable	sum Pi.addCommMonoid	—	Multiset.aemeasurable_sum Multiset.mem_map
measurable_fun_prod 📖	mathematical	Measurable	prod	—	prod_induction Measurable.mul measurable_one
measurable_fun_sum 📖	mathematical	Measurable	sum	—	sum_apply sum_induction Measurable.add measurable_zero
measurable_prod 📖	mathematical	Measurable	prod	—	prod_induction Measurable.mul measurable_one
measurable_prod_apply 📖	mathematical	Measurable Prod.instMeasurableSpace Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase	prod Pi.commMonoid	—	prod_apply measurable_prod Measurable.fun_comp Measurable.prodMk measurable_id'
measurable_sum 📖	mathematical	Measurable	sum	—	sum_apply sum_induction Measurable.add measurable_zero
measurable_sum_apply 📖	mathematical	Measurable Prod.instMeasurableSpace Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase	sum Pi.addCommMonoid	—	sum_apply measurable_sum Measurable.fun_comp Measurable.prodMk measurable_id'

IsAddUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_const_vadd_iff 📖	mathematical	IsAddUnit	AEMeasurable HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	aemeasurable_const_vadd_iff AddUnits.instMeasurableConstVAdd
measurable_const_vadd_iff 📖	mathematical	IsAddUnit	Measurable HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	measurable_const_vadd_iff AddUnits.instMeasurableConstVAdd

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_const_smul_iff 📖	mathematical	IsUnit	AEMeasurable SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	aemeasurable_const_smul_iff Units.instMeasurableConstSMul
measurable_const_smul_iff 📖	mathematical	IsUnit	Measurable SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	measurable_const_smul_iff Units.instMeasurableConstSMul

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_fun_prod 📖	mathematical	AEMeasurable	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne	—	aemeasurable_prod
aemeasurable_fun_sum 📖	mathematical	AEMeasurable	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddZero.toZero	—	Pi.list_sum_apply aemeasurable_sum
aemeasurable_prod 📖	mathematical	AEMeasurable	Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Pi.instOne MulOne.toOne	—	aemeasurable_one AEMeasurable.mul
aemeasurable_sum 📖	mathematical	AEMeasurable	Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Pi.instZero AddZero.toZero	—	aemeasurable_zero AEMeasurable.add
measurable_fun_prod 📖	mathematical	Measurable	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne	—	measurable_prod
measurable_fun_sum 📖	mathematical	Measurable	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddZero.toZero	—	Pi.list_sum_apply measurable_sum
measurable_prod 📖	mathematical	Measurable	Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Pi.instOne MulOne.toOne	—	measurable_one Measurable.mul
measurable_sum 📖	mathematical	Measurable	Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Pi.instZero AddZero.toZero	—	measurable_zero Measurable.add

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	—	Measurable	—	—	comp MeasurableAdd₂.measurable_add prodMk
add' 📖	mathematical	Measurable Prod.instMeasurableSpace Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase	Pi.instAdd	—	add fun_comp prodMk measurable_id'
add_const 📖	—	Measurable	—	—	comp MeasurableAdd.measurable_add_const
add_iff_left 📖	mathematical	Measurable	Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	add_iff_right add_comm
add_iff_right 📖	mathematical	Measurable	Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	add neg add_neg_cancel_comm
const_add 📖	—	Measurable	—	—	comp MeasurableAdd.measurable_const_add
const_div 📖	—	Measurable	—	—	comp MeasurableDiv.measurable_const_div
const_mul 📖	—	Measurable	—	—	comp MeasurableMul.measurable_const_mul
const_pow 📖	—	Measurable	—	—	pow measurable_const
const_smul 📖	mathematical	Measurable	Function.hasSMul	—	comp MeasurableConstSMul.measurable_const_smul
const_sub 📖	—	Measurable	—	—	comp MeasurableSub.measurable_const_sub
const_vadd 📖	mathematical	Measurable	HVAdd.hVAdd instHVAdd Function.hasVAdd	—	comp MeasurableConstVAdd.measurable_const_vadd
div 📖	—	Measurable	—	—	comp MeasurableDiv₂.measurable_div prodMk
div' 📖	mathematical	Measurable Prod.instMeasurableSpace Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase	Pi.instDiv	—	div fun_comp prodMk measurable_id'
div_const 📖	—	Measurable	—	—	comp MeasurableDiv.measurable_div_const
fun_const_smul 📖	mathematical	Measurable Prod.instMeasurableSpace Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase	Function.hasSMul	—	const_smul comp prodMk measurable_id
fun_const_vadd 📖	mathematical	Measurable Prod.instMeasurableSpace Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase	HVAdd.hVAdd instHVAdd Function.hasVAdd	—	const_vadd comp prodMk measurable_id
inv 📖	—	Measurable	—	—	comp MeasurableInv.measurable_inv
measurableSMul₂_iterateAddAct 📖	mathematical	Measurable	MeasurableVAdd₂ IterateAddAct AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid IterateAddAct.instAddCommMonoid AddAction.toAddSemigroupAction IterateAddAct.instAddAction IterateAddAct.instMeasurableSpace	—	measurable_from_prod_countable_left IterateAddAct.instCountable DiscreteMeasurableSpace.toMeasurableSingletonClass IterateAddAct.instDiscreteMeasurableSpace iterate comp measurable_swap
measurableSMul₂_iterateMulAct 📖	mathematical	Measurable	MeasurableSMul₂ IterateMulAct SemigroupAction.toSMul Monoid.toSemigroup CommMonoid.toMonoid IterateMulAct.instCommMonoid MulAction.toSemigroupAction IterateMulAct.instMulAction IterateMulAct.instMeasurableSpace	—	measurable_from_prod_countable_left IterateMulAct.instCountable DiscreteMeasurableSpace.toMeasurableSingletonClass IterateMulAct.instDiscreteMeasurableSpace iterate comp measurable_swap
mul 📖	—	Measurable	—	—	comp MeasurableMul₂.measurable_mul prodMk
mul' 📖	mathematical	Measurable Prod.instMeasurableSpace Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase	Pi.instMul	—	mul fun_comp prodMk measurable_id'
mul_const 📖	—	Measurable	—	—	comp MeasurableMul.measurable_mul_const
mul_iff_left 📖	mathematical	Measurable	Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	mul_iff_right mul_comm
mul_iff_right 📖	mathematical	Measurable	Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	mul inv mul_inv_cancel_comm
neg 📖	—	Measurable	—	—	comp MeasurableNeg.measurable_neg
pow 📖	—	Measurable	—	—	comp MeasurablePow.measurable_pow prodMk
pow_const 📖	—	Measurable	—	—	pow measurable_const
smul 📖	—	Measurable	—	—	comp MeasurableSMul₂.measurable_smul prodMk
smul' 📖	mathematical	Measurable Prod.instMeasurableSpace Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase	Pi.smul'	—	smul fun_comp prodMk measurable_id'
smul_const 📖	—	Measurable	—	—	comp MeasurableSMul.measurable_smul_const
sub 📖	—	Measurable	—	—	comp MeasurableSub₂.measurable_sub prodMk
sub' 📖	mathematical	Measurable Prod.instMeasurableSpace Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase	Pi.instSub	—	sub fun_comp prodMk measurable_id'
sub_const 📖	—	Measurable	—	—	comp MeasurableSub.measurable_sub_const
vadd 📖	mathematical	Measurable	HVAdd.hVAdd instHVAdd	—	comp MeasurableVAdd₂.measurable_vadd prodMk
vadd' 📖	mathematical	Measurable Prod.instMeasurableSpace Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase	HVAdd.hVAdd instHVAdd Pi.vadd'	—	vadd fun_comp prodMk measurable_id'
vadd_const 📖	mathematical	Measurable	HVAdd.hVAdd instHVAdd	—	comp MeasurableVAdd.measurable_vadd_const

MeasurableAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_add_const 📖	mathematical	—	Measurable	—	—
measurable_const_add 📖	mathematical	—	Measurable	—	—

MeasurableAdd₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_add 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	—
toMeasurableAdd 📖	mathematical	—	MeasurableAdd	—	Measurable.add measurable_const measurable_id'

MeasurableConstSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_const_smul 📖	mathematical	—	Measurable	—	—

MeasurableConstVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_const_vadd 📖	mathematical	—	Measurable HVAdd.hVAdd instHVAdd	—	—

MeasurableDiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_const_div 📖	mathematical	—	Measurable	—	—
measurable_div_const 📖	mathematical	—	Measurable	—	—
toMeasurableInv 📖	mathematical	—	MeasurableInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	one_div measurable_const_div

MeasurableDiv₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_div 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	—
toMeasurableDiv 📖	mathematical	—	MeasurableDiv	—	Measurable.div measurable_const measurable_id

MeasurableInv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_inv 📖	mathematical	—	Measurable	—	—

MeasurableMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_const_mul 📖	mathematical	—	Measurable	—	—
measurable_mul_const 📖	mathematical	—	Measurable	—	—

MeasurableMul₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_mul 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	—
toMeasurableMul 📖	mathematical	—	MeasurableMul	—	Measurable.mul measurable_const measurable_id'

MeasurableNeg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_neg 📖	mathematical	—	Measurable	—	—

MeasurablePow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_pow 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	—

MeasurableSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_smul_const 📖	mathematical	—	Measurable	—	—
op 📖	mathematical	—	MeasurableSMul MulOpposite MulOpposite.instMeasurableSpace	—	MulOpposite.instMeasurableConstSMul toMeasurableConstSMul IsCentralScalar.op_smul_eq_smul Measurable.comp measurable_smul_const measurable_mul_unop
toMeasurableConstSMul 📖	mathematical	—	MeasurableConstSMul	—	—

MeasurableSMul₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_smul 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	—
op 📖	mathematical	—	MeasurableSMul₂ MulOpposite MulOpposite.instMeasurableSpace	—	IsCentralScalar.op_smul_eq_smul Measurable.smul Measurable.comp measurable_mul_unop measurable_fst measurable_snd
toMeasurableSMul 📖	mathematical	—	MeasurableSMul	—	Measurable.smul measurable_const measurable_id'

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv 📖	mathematical	MeasurableSet	Set Set.inv	—	MeasurableInv.measurable_inv
neg 📖	mathematical	MeasurableSet	Set Set.neg	—	MeasurableNeg.measurable_neg

MeasurableSub

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_const_sub 📖	mathematical	—	Measurable	—	—
measurable_sub_const 📖	mathematical	—	Measurable	—	—

MeasurableSub₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_sub 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	—
toMeasurableSub 📖	mathematical	—	MeasurableSub	—	Measurable.sub measurable_const measurable_id

MeasurableVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_vadd_const 📖	mathematical	—	Measurable HVAdd.hVAdd instHVAdd	—	—
op 📖	mathematical	—	MeasurableVAdd AddOpposite AddOpposite.instMeasurableSpace	—	AddOpposite.instMeasurableConstVAdd toMeasurableConstVAdd IsCentralVAdd.op_vadd_eq_vadd Measurable.comp measurable_vadd_const measurable_add_unop
toMeasurableConstVAdd 📖	mathematical	—	MeasurableConstVAdd	—	—

MeasurableVAdd₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_vadd 📖	mathematical	—	Measurable Prod.instMeasurableSpace HVAdd.hVAdd instHVAdd	—	—
toMeasurableVAdd 📖	mathematical	—	MeasurableVAdd	—	Measurable.vadd measurable_const measurable_id'

Monoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurablePow 📖	mathematical	—	MeasurablePow Nat.instMeasurableSpace toNatPow	—	measurable_from_prod_countable_left instCountableNat Nat.instMeasurableSingletonClass pow_zero pow_succ Measurable.mul measurable_id

MulOpposite

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	8 math math: MeasurableSMul.op, measurable_mul_op, instMeasurableMul₂, MeasurableSMul₂.op, measurableSMul_opposite_of_mul, measurableSMul₂_opposite_of_mul, instMeasurableMul, measurable_mul_unop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableConstSMul 📖	mathematical	—	MeasurableConstSMul MulOpposite	—	IsCentralScalar.op_smul_eq_smul MeasurableConstSMul.measurable_const_smul
instMeasurableMul 📖	mathematical	—	MeasurableMul MulOpposite instMeasurableSpace instMul	—	Measurable.comp measurable_mul_op Measurable.mul_const measurable_mul_unop Measurable.const_mul
instMeasurableMul₂ 📖	mathematical	—	MeasurableMul₂ MulOpposite instMeasurableSpace instMul	—	Measurable.comp measurable_mul_op Measurable.mul measurable_mul_unop measurable_snd measurable_fst

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_fun_prod 📖	mathematical	AEMeasurable	prod map	—	aemeasurable_prod
aemeasurable_fun_sum 📖	mathematical	AEMeasurable	sum map	—	Pi.multiset_sum_apply aemeasurable_sum
aemeasurable_prod 📖	mathematical	AEMeasurable	prod Pi.commMonoid	—	List.aemeasurable_prod
aemeasurable_sum 📖	mathematical	AEMeasurable	sum Pi.addCommMonoid	—	List.aemeasurable_sum mem_coe
measurable_fun_prod 📖	mathematical	Measurable	prod map	—	measurable_prod
measurable_fun_sum 📖	mathematical	Measurable	sum map	—	Pi.multiset_sum_apply measurable_sum
measurable_prod 📖	mathematical	Measurable	prod Pi.commMonoid	—	List.measurable_prod
measurable_sum 📖	mathematical	Measurable	sum Pi.addCommMonoid	—	List.measurable_sum mem_coe

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableConstSMul 📖	mathematical	MeasurableConstSMul	instSMul MeasurableSpace.pi	—	measurable_pi_iff Measurable.const_smul measurable_pi_apply
instMeasurableConstVAdd 📖	mathematical	MeasurableConstVAdd	instVAdd MeasurableSpace.pi	—	measurable_pi_iff Measurable.const_vadd measurable_pi_apply
measurableAdd 📖	mathematical	MeasurableAdd	MeasurableSpace.pi instAdd	—	measurable_pi_iff Measurable.const_add measurable_pi_apply Measurable.add_const
measurableAdd₂ 📖	mathematical	MeasurableAdd₂	MeasurableSpace.pi instAdd	—	measurable_pi_iff Measurable.add Measurable.eval measurable_fst measurable_snd
measurableDiv 📖	mathematical	MeasurableDiv	MeasurableSpace.pi instDiv	—	measurable_pi_iff Measurable.const_div measurable_pi_apply Measurable.div_const
measurableDiv₂ 📖	mathematical	MeasurableDiv₂	MeasurableSpace.pi instDiv	—	measurable_pi_iff Measurable.div Measurable.eval measurable_fst measurable_snd
measurableInv 📖	mathematical	MeasurableInv	instInv MeasurableSpace.pi	—	measurable_pi_iff Measurable.inv measurable_pi_apply
measurableMul 📖	mathematical	MeasurableMul	MeasurableSpace.pi instMul	—	measurable_pi_iff Measurable.const_mul measurable_pi_apply Measurable.mul_const
measurableMul₂ 📖	mathematical	MeasurableMul₂	MeasurableSpace.pi instMul	—	measurable_pi_iff Measurable.mul Measurable.eval measurable_fst measurable_snd
measurableNeg 📖	mathematical	MeasurableNeg	instNeg MeasurableSpace.pi	—	measurable_pi_iff Measurable.neg measurable_pi_apply
measurableSMul 📖	mathematical	MeasurableSMul	instSMul MeasurableSpace.pi	—	instMeasurableConstSMul MeasurableSMul.toMeasurableConstSMul measurable_pi_iff MeasurableSMul.measurable_smul_const
measurableSub 📖	mathematical	MeasurableSub	MeasurableSpace.pi instSub	—	measurable_pi_iff Measurable.const_sub measurable_pi_apply Measurable.sub_const
measurableSub₂ 📖	mathematical	MeasurableSub₂	MeasurableSpace.pi instSub	—	measurable_pi_iff Measurable.sub Measurable.eval measurable_fst measurable_snd
measurableVAdd 📖	mathematical	MeasurableVAdd	instVAdd MeasurableSpace.pi	—	instMeasurableConstVAdd MeasurableVAdd.toMeasurableConstVAdd measurable_pi_iff MeasurableVAdd.measurable_vadd_const

SubNegMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSMul_int₂ 📖	mathematical	—	MeasurableSMul₂ toZSMul Int.instMeasurableSpace	—	measurable_from_prod_countable_left instCountableInt Int.instMeasurableSingletonClass natCast_zsmul MeasurableConstSMul.measurable_const_smul MeasurableSMul.toMeasurableConstSMul MeasurableSMul₂.toMeasurableSMul AddMonoid.measurableSMul_nat₂ negSucc_zsmul Measurable.neg Measurable.comp measurable_swap

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableConstSMul 📖	mathematical	—	MeasurableConstSMul Subgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MulAction.toSemigroupAction instMulAction	—	Submonoid.instMeasurableConstSMul
instMeasurableSMul 📖	mathematical	—	MeasurableSMul Subgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MulAction.toSemigroupAction instMulAction Subtype.instMeasurableSpace	—	Submonoid.instMeasurableSMul

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableConstSMul 📖	mathematical	—	MeasurableConstSMul Submonoid Monoid.toMulOneClass SetLike.instMembership instSetLike smul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	MeasurableConstSMul.measurable_const_smul
instMeasurableSMul 📖	mathematical	—	MeasurableSMul Submonoid Monoid.toMulOneClass SetLike.instMembership instSetLike smul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Subtype.instMeasurableSpace	—	instMeasurableConstSMul MeasurableSMul.toMeasurableConstSMul Measurable.comp MeasurableSMul.measurable_smul_const measurable_subtype_coe

Units

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	1 math math: measurableSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableConstSMul 📖	mathematical	—	MeasurableConstSMul Units instSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	MeasurableConstSMul.measurable_const_smul
measurableSMul 📖	mathematical	—	MeasurableSMul Units instSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction instMeasurableSpace	—	instMeasurableConstSMul MeasurableSMul.toMeasurableConstSMul Measurable.comp MeasurableSMul.measurable_smul_const MeasurableSpace.le_map_comap

(root)

Definitions

Name	Category	Theorems
MeasurableAdd 📖	CompData	4 math math: ContinuousAdd.measurableAdd, AddOpposite.instMeasurableAdd, MeasurableAdd₂.toMeasurableAdd, DiscreteMeasurableSpace.toMeasurableAdd
MeasurableAdd₂ 📖	CompData	5 math math: MeasureTheory.Measure.instMeasurableAdd₂, EReal.instMeasurableAdd₂, ContinuousAdd.measurableMul₂, DiscreteMeasurableSpace.toMeasurableAdd₂, AddOpposite.instMeasurableMul₂
MeasurableConstSMul 📖	CompData	6 math math: MulOpposite.instMeasurableConstSMul, Subgroup.instMeasurableConstSMul, Units.instMeasurableConstSMul, Submonoid.instMeasurableConstSMul, ContinuousConstSMul.toMeasurableConstSMul, MeasurableSMul.toMeasurableConstSMul
MeasurableConstVAdd 📖	CompData	6 math math: MeasurableVAdd.toMeasurableConstVAdd, AddSubgroup.instMeasurableConstVAdd, ContinuousConstVAdd.toMeasurableConstVAdd, AddSubmonoid.instMeasurableConstVAdd, AddOpposite.instMeasurableConstVAdd, AddUnits.instMeasurableConstVAdd
MeasurableDiv 📖	CompData	3 math math: DiscreteMeasurableSpace.toMeasurableDiv, measurableDiv_of_mul_inv, MeasurableDiv₂.toMeasurableDiv
MeasurableDiv₂ 📖	CompData	2 math math: DiscreteMeasurableSpace.toMeasurableDiv₂, measurableDiv₂_of_mul_inv
MeasurableInv 📖	CompData	6 math math: DiscreteMeasurableSpace.toMeasurableInv, ENNReal.instMeasurableInv, ContinuousInv.measurableInv, HasContinuousInv₀.measurableInv, ContinuousInv₀.measurableInv, MeasurableDiv.toMeasurableInv
MeasurableMul 📖	CompData	4 math math: MeasurableMul₂.toMeasurableMul, DiscreteMeasurableSpace.toMeasurableMul, MulOpposite.instMeasurableMul, ContinuousMul.measurableMul
MeasurableMul₂ 📖	CompData	5 math math: EReal.instMeasurableMul₂, MulOpposite.instMeasurableMul₂, ENNReal.instMeasurableMul₂, ContinuousMul.measurableMul₂, DiscreteMeasurableSpace.toMeasurableMul₂
MeasurableNeg 📖	CompData	2 math math: DiscreteMeasurableSpace.toMeasurableNeg, ContinuousNeg.measurableNeg
MeasurablePow 📖	CompData	6 math math: Real.hasMeasurablePow, ENNReal.hasMeasurablePow, DivInvMonoid.measurableZPow, Monoid.measurablePow, NNReal.hasMeasurablePow, Complex.hasMeasurablePow
MeasurableSMul 📖	CompData	11 math math: MeasurableSMul.op, Submonoid.instMeasurableSMul, MeasurableSMul₂.toMeasurableSMul, measurableSMul_opposite_of_mul, QuotientGroup.measurableSMul, Units.measurableSMul, measurableSMul_iterateMulAct, measurableSMul_of_mul, Subgroup.instMeasurableSMul, ContinuousSMul.toMeasurableSMul, ENNReal.instMeasurableSMulNNReal
MeasurableSMul₂ 📖	CompData	9 math math: MeasurableSMul₂.op, SubNegMonoid.measurableSMul_int₂, measurableSMul₂_iterateMulAct, measurableSMul₂_of_mul, NNReal.instMeasurableSMul₂ENNReal, measurableSMul₂_opposite_of_mul, ContinuousSMul.measurableSMul₂, AddMonoid.measurableSMul_nat₂, Measurable.measurableSMul₂_iterateMulAct
MeasurableSub 📖	CompData	4 math math: ContinuousSub.measurableSub, measurableSub_of_add_neg, DiscreteMeasurableSpace.toMeasurableSub, MeasurableSub₂.toMeasurableSub
MeasurableSub₂ 📖	CompData	4 math math: ContinuousSub.measurableSub₂, DiscreteMeasurableSpace.toMeasurableSub₂, ENNReal.instMeasurableSub₂, measurableDiv₂_of_add_neg
MeasurableVAdd 📖	CompData	10 math math: MeasurableVAdd₂.toMeasurableVAdd, QuotientAddGroup.measurableVAdd, measurableVAdd_iterateAddAct, MeasurableVAdd.op, AddSubgroup.instMeasurableVAdd, AddUnits.measurableVAdd, ContinuousVAdd.toMeasurableVAdd, AddSubmonoid.instMeasurableVAdd, measurableVAdd_opposite_of_add, measurableVAdd_of_add
MeasurableVAdd₂ 📖	CompData	4 math math: Measurable.measurableSMul₂_iterateAddAct, measurableSMul₂_of_add, measurableSMul₂_iterateAddAct, measurableSMul₂_opposite_of_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_const_smul_iff 📖	mathematical	—	AEMeasurable SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	inv_smul_smul AEMeasurable.const_smul
aemeasurable_const_smul_iff₀ 📖	mathematical	—	AEMeasurable SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	—	IsUnit.aemeasurable_const_smul_iff
aemeasurable_const_vadd_iff 📖	mathematical	—	AEMeasurable HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	neg_vadd_vadd AEMeasurable.const_vadd
aemeasurable_inv_iff 📖	mathematical	—	AEMeasurable InvolutiveInv.toInv	—	inv_inv AEMeasurable.inv
aemeasurable_neg_iff 📖	mathematical	—	AEMeasurable InvolutiveNeg.toNeg	—	neg_neg AEMeasurable.neg
instMeasurableEqOfCanonicallyOrderedAddOfOrderedSubOfMeasurableSub₂OfMeasurableSingletonClass 📖	mathematical	—	MeasurableEq	—	Measurable.and Measurable.eq_const Measurable.sub Measurable.fst measurable_id' Measurable.snd
instMeasurableEqOfMeasurableSingletonClassOfMeasurableSub₂ 📖	mathematical	—	MeasurableEq	—	Measurable.eq_const Measurable.sub Measurable.fst measurable_id' Measurable.snd
measurableDiv_of_mul_inv 📖	mathematical	—	MeasurableDiv DivInvMonoid.toDiv	—	div_eq_mul_inv Measurable.const_mul MeasurableInv.measurable_inv Measurable.mul_const measurable_id
measurableDiv₂_of_add_neg 📖	mathematical	—	MeasurableSub₂ SubNegMonoid.toSub	—	sub_eq_add_neg Measurable.add measurable_fst Measurable.neg measurable_snd
measurableDiv₂_of_mul_inv 📖	mathematical	—	MeasurableDiv₂ DivInvMonoid.toDiv	—	div_eq_mul_inv Measurable.mul measurable_fst Measurable.inv measurable_snd
measurableEmbedding_inv 📖	mathematical	—	MeasurableEmbedding InvolutiveInv.toInv	—	inv_injective MeasurableInv.measurable_inv MeasurableSet.inv Set.image_inv_eq_inv
measurableEmbedding_neg 📖	mathematical	—	MeasurableEmbedding InvolutiveNeg.toNeg	—	neg_injective MeasurableNeg.measurable_neg MeasurableSet.neg Set.image_neg_eq_neg
measurableSMul_iterateMulAct 📖	mathematical	—	MeasurableSMul IterateMulAct SemigroupAction.toSMul Monoid.toSemigroup CommMonoid.toMonoid IterateMulAct.instCommMonoid MulAction.toSemigroupAction IterateMulAct.instMulAction IterateMulAct.instMeasurableSpace Measurable	—	MeasurableConstSMul.measurable_const_smul MeasurableSMul.toMeasurableConstSMul Measurable.measurableSMul₂_iterateMulAct MeasurableSMul₂.toMeasurableSMul
measurableSMul_of_mul 📖	mathematical	—	MeasurableSMul	—	Measurable.const_mul measurable_id' Measurable.mul_const
measurableSMul_opposite_of_mul 📖	mathematical	—	MeasurableSMul MulOpposite Mul.toSMulMulOpposite MulOpposite.instMeasurableSpace	—	Measurable.mul_const measurable_id' Measurable.const_mul measurable_mul_unop
measurableSMul₂_iterateAddAct 📖	mathematical	—	MeasurableVAdd₂ IterateAddAct AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid IterateAddAct.instAddCommMonoid AddAction.toAddSemigroupAction IterateAddAct.instAddAction IterateAddAct.instMeasurableSpace Measurable	—	measurableVAdd_iterateAddAct MeasurableVAdd₂.toMeasurableVAdd Measurable.measurableSMul₂_iterateAddAct
measurableSMul₂_iterateMulAct 📖	mathematical	—	MeasurableSMul₂ IterateMulAct SemigroupAction.toSMul Monoid.toSemigroup CommMonoid.toMonoid IterateMulAct.instCommMonoid MulAction.toSemigroupAction IterateMulAct.instMulAction IterateMulAct.instMeasurableSpace Measurable	—	measurableSMul_iterateMulAct MeasurableSMul₂.toMeasurableSMul Measurable.measurableSMul₂_iterateMulAct
measurableSMul₂_of_add 📖	mathematical	—	MeasurableVAdd₂ Add.toVAdd	—	MeasurableAdd₂.measurable_add
measurableSMul₂_of_mul 📖	mathematical	—	MeasurableSMul₂	—	MeasurableMul₂.measurable_mul
measurableSMul₂_opposite_of_add 📖	mathematical	—	MeasurableVAdd₂ AddOpposite Add.toVAddAddOpposite AddOpposite.instMeasurableSpace	—	Measurable.add measurable_snd Measurable.comp measurable_add_unop measurable_fst
measurableSMul₂_opposite_of_mul 📖	mathematical	—	MeasurableSMul₂ MulOpposite Mul.toSMulMulOpposite MulOpposite.instMeasurableSpace	—	Measurable.mul measurable_snd Measurable.comp measurable_mul_unop measurable_fst
measurableSet_eq_fun' 📖	mathematical	Measurable	MeasurableSet setOf	—	measurableSet_eq_fun
measurableSet_eq_fun_of_countable 📖	mathematical	Measurable	MeasurableSet setOf	—	measurableSet_eq_fun
measurableSub_of_add_neg 📖	mathematical	—	MeasurableSub SubNegMonoid.toSub	—	sub_eq_add_neg Measurable.const_add MeasurableNeg.measurable_neg Measurable.add_const measurable_id
measurableVAdd_iterateAddAct 📖	mathematical	—	MeasurableVAdd IterateAddAct AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid IterateAddAct.instAddCommMonoid AddAction.toAddSemigroupAction IterateAddAct.instAddAction IterateAddAct.instMeasurableSpace Measurable	—	MeasurableConstVAdd.measurable_const_vadd MeasurableVAdd.toMeasurableConstVAdd Measurable.measurableSMul₂_iterateAddAct MeasurableVAdd₂.toMeasurableVAdd
measurableVAdd_of_add 📖	mathematical	—	MeasurableVAdd Add.toVAdd	—	Measurable.const_add measurable_id' Measurable.add_const
measurableVAdd_opposite_of_add 📖	mathematical	—	MeasurableVAdd AddOpposite Add.toVAddAddOpposite AddOpposite.instMeasurableSpace	—	Measurable.add_const measurable_id' Measurable.const_add measurable_add_unop
measurable_add_op 📖	mathematical	—	Measurable AddOpposite AddOpposite.instMeasurableSpace AddOpposite.op	—	—
measurable_add_unop 📖	mathematical	—	Measurable AddOpposite AddOpposite.instMeasurableSpace AddOpposite.unop	—	—
measurable_const_smul_iff 📖	mathematical	—	Measurable SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	inv_smul_smul Measurable.const_smul
measurable_const_smul_iff₀ 📖	mathematical	—	Measurable SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	—	IsUnit.measurable_const_smul_iff
measurable_const_vadd_iff 📖	mathematical	—	Measurable HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	neg_vadd_vadd Measurable.const_vadd
measurable_div_const' 📖	mathematical	—	Measurable DivInvMonoid.toDiv	—	div_eq_mul_inv
measurable_inv_iff 📖	mathematical	—	Measurable InvolutiveInv.toInv	—	inv_inv Measurable.inv
measurable_mul_op 📖	mathematical	—	Measurable MulOpposite MulOpposite.instMeasurableSpace MulOpposite.op	—	—
measurable_mul_unop 📖	mathematical	—	Measurable MulOpposite MulOpposite.instMeasurableSpace MulOpposite.unop	—	—
measurable_neg_iff 📖	mathematical	—	Measurable InvolutiveNeg.toNeg	—	neg_neg Measurable.neg
measurable_sub_const' 📖	mathematical	—	Measurable SubNegMonoid.toSub	—	sub_eq_add_neg MeasurableAdd.measurable_add_const

---

← Back to Index