Documentation Verification Report

Module

📁 Source: Mathlib/Topology/Algebra/InfiniteSum/Module.lean

Statistics

Metric	Count
Definitions `automorphize`, `automorphize`, `automorphize`, `automorphize`	4
Theorems `automorphize_smul_left`, `hasSum`, `hasSum'`, `map_tsum`, `summable`, `tsum_eq_iff`, `hasSum`, `map_tsum`, `summable`, `const_smul`, `mapL`, `smul`, `smul_const`, `smul_eq`, `automorphize_smul_left`, `automorphize_smul_left`, `automorphize_smul_left`, `const_smul`, `mapL`, `smul_const`, `tsum_const_smul`, `tsum_smul_const`, `tsum_const_smul'`, `tsum_const_smul''`, `tsum_smul_tsum`	25
Total	29

AddAction

Definitions

Name	Category	Theorems
`automorphize` 📖	CompOp	1 math math: `automorphize_smul_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`automorphize_smul_left` 📖	mathematical	—	`automorphize` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `orbitRel`	—	`Quotient.eq` `tsum_const_smul''`

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum` 📖	mathematical	—	`HasSum` `DFunLike.coe` `ContinuousLinearEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`symm_apply_apply` `HasSum.mapL` `apply_symm_apply` `ContinuousLinearMap.hasSum`
`hasSum'` 📖	mathematical	—	`HasSum` `DFunLike.coe` `ContinuousLinearEquiv` `EquivLike.toFunLike` `equivLike`	—	`hasSum` `symm_apply_apply`
`map_tsum` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `EquivLike.toFunLike` `equivLike` `tsum`	—	`symm` `IsEquiv.toSymm` `eq_isEquiv` `tsum_eq_iff` `symm_apply_apply`
`summable` 📖	mathematical	—	`Summable` `DFunLike.coe` `ContinuousLinearEquiv` `EquivLike.toFunLike` `equivLike`	—	`HasSum.summable` `hasSum` `Summable.hasSum` `ContinuousLinearMap.summable`
`tsum_eq_iff` 📖	mathematical	—	`tsum` `DFunLike.coe` `ContinuousLinearEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`HasSum.tsum_eq` `hasSum` `Summable.hasSum_iff` `summable` `tsum_bot` `AddEquiv.map_finsum` `tsum_eq_zero_of_not_summable` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `continuousSemilinearEquivClass` `apply_symm_apply`

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum` 📖	mathematical	`HasSum`	`HasSum` `DFunLike.coe` `ContinuousLinearMap` `funLike`	—	`HasSum.map` `AddMonoidHom.instAddMonoidHomClass` `continuous`
`map_tsum` 📖	mathematical	`Summable`	`DFunLike.coe` `ContinuousLinearMap` `funLike` `tsum`	—	`HasSum.tsum_eq` `HasSum.mapL` `Summable.hasSum`
`summable` 📖	mathematical	`Summable`	`Summable` `DFunLike.coe` `ContinuousLinearMap` `funLike`	—	`HasSum.summable` `HasSum.mapL` `Summable.hasSum`

HasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul` 📖	mathematical	`HasSum`	`HasSum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass`	—	`map` `AddMonoidHom.instAddMonoidHomClass` `ContinuousConstSMul.continuous_const_smul`
`mapL` 📖	mathematical	`HasSum`	`HasSum` `DFunLike.coe` `ContinuousLinearMap` `ContinuousLinearMap.funLike`	—	`ContinuousLinearMap.hasSum`
`smul` 📖	mathematical	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SummationFilter.unconditional` `Summable` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`HasSum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SummationFilter.unconditional`	—	`smul_eq`
`smul_const` 📖	mathematical	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`HasSum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`map` `AddMonoidHom.instAddMonoidHomClass` `Continuous.smul` `continuous_id` `continuous_const`
`smul_eq` 📖	mathematical	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SummationFilter.unconditional` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`smul_const` `const_smul` `ContinuousSMul.continuousConstSMul` `prod_fiberwise` `T3Space.toRegularSpace` `unique` `T25Space.t2Space` `T3Space.t25Space` `SummationFilter.instNeBotUnconditional`

MulAction

Definitions

Name	Category	Theorems
`automorphize` 📖	CompOp	1 math math: `automorphize_smul_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`automorphize_smul_left` 📖	mathematical	—	`automorphize` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `orbitRel`	—	`Quotient.eq` `tsum_const_smul''`

QuotientAddGroup

Definitions

Name	Category	Theorems
`automorphize` 📖	CompOp	3 math math: `integral_eq_integral_automorphize`, `automorphize_smul_left`, `integral_mul_eq_integral_automorphize_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`automorphize_smul_left` 📖	mathematical	—	`automorphize` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `leftRel`	—	`AddAction.automorphize_smul_left`

QuotientGroup

Definitions

Name	Category	Theorems
`automorphize` 📖	CompOp	3 math math: `integral_eq_integral_automorphize`, `automorphize_smul_left`, `integral_mul_eq_integral_automorphize_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`automorphize_smul_left` 📖	mathematical	—	`automorphize` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `leftRel`	—	`MulAction.automorphize_smul_left`

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul` 📖	mathematical	`Summable`	`Summable` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass`	—	`HasSum.summable` `HasSum.const_smul` `hasSum`
`mapL` 📖	mathematical	`Summable`	`Summable` `DFunLike.coe` `ContinuousLinearMap` `ContinuousLinearMap.funLike`	—	`ContinuousLinearMap.summable`
`smul_const` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Summable` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`HasSum.summable` `HasSum.smul_const` `hasSum`
`tsum_const_smul` 📖	mathematical	`Summable`	`tsum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass`	—	`HasSum.tsum_eq` `HasSum.const_smul` `hasSum`
`tsum_smul_const` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`tsum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`HasSum.tsum_eq` `HasSum.smul_const` `hasSum`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tsum_const_smul'` 📖	mathematical	—	`tsum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`inv_smul_smul` `smul_inv_smul` `AddMonoidHom.map_add'` `Topology.IsClosedEmbedding.map_tsum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `Homeomorph.isClosedEmbedding`
`tsum_const_smul''` 📖	mathematical	—	`tsum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Module.toDistribMulAction`	—	`eq_or_ne` `zero_smul` `tsum_zero` `tsum_const_smul'` `Units.continuousConstSMul`
`tsum_smul_tsum` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SummationFilter.unconditional` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `tsum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SummationFilter.unconditional`	—	`HasSum.smul_eq` `Summable.hasSum`

---

← Back to Index