Documentation Verification Report

Convolution

📁 Source: Mathlib/RingTheory/Coalgebra/Convolution.lean

Statistics

Metric	Count
Definitions `convCommRing`, `convCommSemiring`, `convMul`, `convNonUnitalNonAssocRing`, `convNonUnitalNonAssocSemiring`, `convNonUnitalRing`, `convNonUnitalSemiring`, `convOne`, `convRing`, `convSemiring`	10
Theorems `convMul_apply`, `algHom_comp_convMul_distrib`, `convMul_apply`, `convMul_comp_coalgHom_distrib`, `convMul_def`, `convOne_apply`, `convOne_def`, `nonUnitalAlgHom_comp_convMul_distrib`, `toSpanSingleton_convMul_toSpanSingleton`, `map_convMul_map`	10
Total	20

Coalgebra.Repr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convMul_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `LinearMap.instFunLike` `WithConv.ofConv` `WithConv` `LinearMap.convMul` `Finset.sum` `ι` `index` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `left` `right`	—	`eq` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_congr`

LinearMap

Definitions

Name	Category	Theorems
`convCommRing` 📖	CompOp	—
`convCommSemiring` 📖	CompOp	—
`convMul` 📖	CompOp	12 math math: `convMul_def`, `Matrix.toLin'_hadamard`, `WithConv.matrixToLin'StarAlgEquiv_apply`, `intrinsicStar_convMul`, `Coalgebra.Repr.convMul_apply`, `nonUnitalAlgHom_comp_convMul_distrib`, `WithConv.symm_matrixToLin'StarAlgEquiv_apply`, `TensorProduct.map_convMul_map`, `toSpanSingleton_convMul_toSpanSingleton`, `convMul_comp_coalgHom_distrib`, `algHom_comp_convMul_distrib`, `convMul_apply`
`convNonUnitalNonAssocRing` 📖	CompOp	—
`convNonUnitalNonAssocSemiring` 📖	CompOp	2 math math: `WithConv.matrixToLin'StarAlgEquiv_apply`, `WithConv.symm_matrixToLin'StarAlgEquiv_apply`
`convNonUnitalRing` 📖	CompOp	—
`convNonUnitalSemiring` 📖	CompOp	—
`convOne` 📖	CompOp	2 math math: `convOne_apply`, `convOne_def`
`convRing` 📖	CompOp	—
`convSemiring` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algHom_comp_convMul_distrib` 📖	mathematical	—	`comp` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `RingHom.id` `RingHomCompTriple.ids` `AlgHom.toLinearMap` `WithConv.ofConv` `LinearMap` `WithConv` `convMul` `Algebra.to_smulCommClass` `IsScalarTower.right` `WithConv.toConv`	—	`RingHomCompTriple.ids` `Algebra.to_smulCommClass` `IsScalarTower.right` `comp.congr_simp` `AlgHom.comp_mul'` `TensorProduct.map_comp`
`convMul_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `WithConv.ofConv` `WithConv` `convMul` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `mul'` `TensorProduct.map` `CoalgebraStruct.comul`	—	—
`convMul_comp_coalgHom_distrib` 📖	mathematical	—	`comp` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `WithConv.ofConv` `LinearMap` `WithConv` `convMul` `Coalgebra.toCoalgebraStruct` `CoalgHom.toLinearMap` `WithConv.toConv`	—	`RingHomCompTriple.ids` `CoalgHomClass.toSemilinearMapClass` `CoalgHom.coalgHomClass` `comp.congr_simp` `TensorProduct.map_comp` `CoalgHomClass.map_comp_comul`
`convMul_def` 📖	mathematical	—	`WithConv` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `convMul` `WithConv.toConv` `comp` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHomCompTriple.ids` `mul'` `TensorProduct.map` `WithConv.ofConv` `CoalgebraStruct.comul`	—	—
`convOne_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `instFunLike` `WithConv.ofConv` `WithConv` `convOne` `RingHom` `RingHom.instFunLike` `algebraMap` `Semiring.toModule` `CoalgebraStruct.counit` `Coalgebra.toCoalgebraStruct`	—	—
`convOne_def` 📖	mathematical	—	`WithConv` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `convOne` `WithConv.toConv` `comp` `Semiring.toModule` `RingHomCompTriple.ids` `Algebra.linearMap` `CoalgebraStruct.counit` `Coalgebra.toCoalgebraStruct`	—	—
`nonUnitalAlgHom_comp_convMul_distrib` 📖	mathematical	—	`comp` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `SemilinearMapClass.semilinearMap` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.toDistribMulAction` `NonUnitalAlgHom.instFunLike_1` `NonUnitalAlgHomClass.instLinearMapClass` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass` `WithConv.ofConv` `LinearMap` `WithConv` `convMul` `Coalgebra.toCoalgebraStruct` `WithConv.toConv`	—	`RingHomCompTriple.ids` `NonUnitalAlgHomClass.instLinearMapClass` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass` `comp.congr_simp` `NonUnitalAlgHom.comp_mul'` `TensorProduct.map_comp`
`toSpanSingleton_convMul_toSpanSingleton` 📖	mathematical	—	`WithConv` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `convMul` `Coalgebra.toCoalgebraStruct` `CommSemiring.toCoalgebra` `WithConv.toConv` `toSpanSingleton` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`WithConv.ext` `ext_ring` `one_smul`

TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_convMul_map` 📖	mathematical	—	`WithConv` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `addCommMonoid` `instModule` `LinearMap.convMul` `Algebra.TensorProduct.instNonUnitalNonAssocSemiring` `Algebra.TensorProduct.sMulCommClass_right` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.TensorProduct.isScalarTower_right` `instCoalgebraStruct` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `WithConv.toConv` `map` `WithConv.ofConv`	—	`Algebra.TensorProduct.sMulCommClass_right` `Algebra.TensorProduct.isScalarTower_right` `IsScalarTower.left` `RingHomCompTriple.ids` `IsScalarTower.to_smulCommClass'` `IsScalarTower.to_smulCommClass` `isScalarTower` `RingHomInvPair.ids` `smulCommClass_left` `LinearMap.comp.congr_simp` `LinearMap.mul'_tensor` `LinearMap.comp_assoc` `tensorTensorTensorComm_trans_tensorTensorTensorComm` `map_comp`

---

← Back to Index