Documentation Verification Report

Action

📁 Source: FLT/Mathlib/MeasureTheory/Group/Action.lean

Statistics

Metric	Count
Definitions	0
Theorems `isAddLeftInvariant_comap`, `isAddRightInvariant_comap`, `isMulLeftInvariant_comap`, `isMulRightInvariant_comap`, `index_mul_addHaar_addSubgroup`, `index_mul_addHaar_addSubgroup_eq_addHaar_addSubgroup`, `index_mul_haar_subgroup`, `index_mul_haar_subgroup_eq_haar_subgroup`, `instMeasurableAddSubtypeMemAddSubgroup_fLT`, `instMeasurableInvSubtypeMemSubgroup_fLT`, `instMeasurableMulSubtypeMemSubgroup_fLT`, `instMeasurableMul₂SubtypeMemAddSubgroup_fLT`, `instMeasurableMul₂SubtypeMemSubgroup_fLT`, `instMeasurableNegSubtypeMemAddSubgroup_fLT`, `isAddLeftInvariant_subtypeVal`, `isAddRightInvariant_subtypeVal`, `isMulLeftInvariant_subtypeVal`, `isMulRightInvariant_subtypeVal`	18
Total	18

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddLeftInvariant_comap` 📖	—	—	—	—	—
`isAddRightInvariant_comap` 📖	—	—	—	—	—
`isMulLeftInvariant_comap` 📖	—	—	—	—	—
`isMulRightInvariant_comap` 📖	—	—	—	—	—

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`index_mul_addHaar_addSubgroup` 📖	—	—	—	—	—
`index_mul_addHaar_addSubgroup_eq_addHaar_addSubgroup` 📖	—	—	—	—	`isAddLeftInvariant_subtypeVal` `index_mul_addHaar_addSubgroup` `instMeasurableAddSubtypeMemAddSubgroup_fLT`
`index_mul_haar_subgroup` 📖	—	—	—	—	—
`index_mul_haar_subgroup_eq_haar_subgroup` 📖	—	—	—	—	`isMulLeftInvariant_subtypeVal` `index_mul_haar_subgroup` `instMeasurableMulSubtypeMemSubgroup_fLT`
`instMeasurableAddSubtypeMemAddSubgroup_fLT` 📖	—	—	—	—	—
`instMeasurableInvSubtypeMemSubgroup_fLT` 📖	—	—	—	—	—
`instMeasurableMulSubtypeMemSubgroup_fLT` 📖	—	—	—	—	—
`instMeasurableMul₂SubtypeMemAddSubgroup_fLT` 📖	—	—	—	—	—
`instMeasurableMul₂SubtypeMemSubgroup_fLT` 📖	—	—	—	—	—
`instMeasurableNegSubtypeMemAddSubgroup_fLT` 📖	—	—	—	—	—
`isAddLeftInvariant_subtypeVal` 📖	—	—	—	—	`MeasurableEmbedding.isAddLeftInvariant_comap` `instMeasurableAddSubtypeMemAddSubgroup_fLT`
`isAddRightInvariant_subtypeVal` 📖	—	—	—	—	`MeasurableEmbedding.isAddRightInvariant_comap` `instMeasurableAddSubtypeMemAddSubgroup_fLT`
`isMulLeftInvariant_subtypeVal` 📖	—	—	—	—	`MeasurableEmbedding.isMulLeftInvariant_comap` `instMeasurableMulSubtypeMemSubgroup_fLT`
`isMulRightInvariant_subtypeVal` 📖	—	—	—	—	`MeasurableEmbedding.isMulRightInvariant_comap` `instMeasurableMulSubtypeMemSubgroup_fLT`

---

← Back to Index