Documentation Verification Report

IterateAct

📁 Source: Mathlib/GroupTheory/GroupAction/IterateAct.lean

Statistics

Metric	Count
Definitions `IterateAddAct`, `instAddAction`, `instAddCommMonoid`, `val`, `IterateMulAct`, `instCommMonoid`, `instMulAction`, `val`	8
Theorems `ext`, `ext_iff`, `instCountable`, `mk_vadd`, `ext`, `ext_iff`, `instCountable`, `mk_smul`	8
Total	16

IterateAddAct

Definitions

Name	Category	Theorems
`instAddAction` 📖	CompOp	6 math math: `measurableVAdd_iterateAddAct`, `Measurable.measurableSMul₂_iterateAddAct`, `MeasureTheory.vaddInvariantMeasure_iterateAddAct`, `MeasureTheory.MeasurePreserving.vaddInvariantMeasure_iterateAddAct`, `measurableSMul₂_iterateAddAct`, `mk_vadd`
`instAddCommMonoid` 📖	CompOp	6 math math: `measurableVAdd_iterateAddAct`, `Measurable.measurableSMul₂_iterateAddAct`, `MeasureTheory.vaddInvariantMeasure_iterateAddAct`, `MeasureTheory.MeasurePreserving.vaddInvariantMeasure_iterateAddAct`, `measurableSMul₂_iterateAddAct`, `mk_vadd`
`val` 📖	CompOp	1 math math: `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`
`instCountable` 📖	mathematical	—	`Countable` `IterateAddAct`	—	`Function.Injective.countable` `instCountableNat` `ext`
`mk_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `IterateAddAct` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `AddAction.toAddSemigroupAction` `instAddAction` `Nat.iterate`	—	—

IterateMulAct

Definitions

Name	Category	Theorems
`instCommMonoid` 📖	CompOp	7 math math: `MeasureTheory.smulInvariantMeasure_iterateMulAct`, `MeasureTheory.MeasurePreserving.smulInvariantMeasure_iterateMulAct`, `measurableSMul₂_iterateMulAct`, `mk_smul`, `measurableSMul_iterateMulAct`, `MeasureTheory.ergodicSMul_iterateMulAct`, `Measurable.measurableSMul₂_iterateMulAct`
`instMulAction` 📖	CompOp	7 math math: `MeasureTheory.smulInvariantMeasure_iterateMulAct`, `MeasureTheory.MeasurePreserving.smulInvariantMeasure_iterateMulAct`, `measurableSMul₂_iterateMulAct`, `mk_smul`, `measurableSMul_iterateMulAct`, `MeasureTheory.ergodicSMul_iterateMulAct`, `Measurable.measurableSMul₂_iterateMulAct`
`val` 📖	CompOp	1 math math: `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`
`instCountable` 📖	mathematical	—	`Countable` `IterateMulAct`	—	`Function.Injective.countable` `instCountableNat` `ext`
`mk_smul` 📖	mathematical	—	`IterateMulAct` `SemigroupAction.toSMul` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid` `MulAction.toSemigroupAction` `instMulAction` `Nat.iterate`	—	—

(root)

Definitions

Name	Category	Theorems
`IterateAddAct` 📖	CompData	8 math math: `IterateAddAct.instDiscreteMeasurableSpace`, `measurableVAdd_iterateAddAct`, `Measurable.measurableSMul₂_iterateAddAct`, `MeasureTheory.vaddInvariantMeasure_iterateAddAct`, `IterateAddAct.instCountable`, `MeasureTheory.MeasurePreserving.vaddInvariantMeasure_iterateAddAct`, `measurableSMul₂_iterateAddAct`, `IterateAddAct.mk_vadd`
`IterateMulAct` 📖	CompData	9 math math: `MeasureTheory.smulInvariantMeasure_iterateMulAct`, `MeasureTheory.MeasurePreserving.smulInvariantMeasure_iterateMulAct`, `measurableSMul₂_iterateMulAct`, `IterateMulAct.mk_smul`, `measurableSMul_iterateMulAct`, `MeasureTheory.ergodicSMul_iterateMulAct`, `IterateMulAct.instCountable`, `IterateMulAct.instDiscreteMeasurableSpace`, `Measurable.measurableSMul₂_iterateMulAct`

---

← Back to Index