Documentation Verification Report

Module

📁 Source: Mathlib/LinearAlgebra/Matrix/Module.lean

Statistics

Metric	Count
Definitions `mapMatrixModule`, `matrixModule`	2
Theorems `mapMatrixModule_apply`, `mapMatrixModule_comp`, `mapMatrixModule_comp_apply`, `mapMatrixModule_id`, `mapMatrixModule_id_apply`, `diagonal_const_smul`, `instIsScalarTowerForall`, `scalar_smul`, `single_smul`, `smul_apply`, `smul_def`, `smul_def'`	12
Total	14

LinearMap

Definitions

Name	Category	Theorems
`mapMatrixModule` 📖	CompOp	6 math math: `ModuleCat.toMatrixModCat_map`, `mapMatrixModule_apply`, `mapMatrixModule_id_apply`, `mapMatrixModule_comp`, `mapMatrixModule_id`, `mapMatrixModule_comp_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapMatrixModule_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Matrix` `Matrix.semiring` `Ring.toSemiring` `RingHom.id` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Matrix.Module.matrixModule` `instFunLike` `mapMatrixModule` `Pi.Function.module` `compLeft`	—	—
`mapMatrixModule_comp` 📖	mathematical	—	`mapMatrixModule` `comp` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Matrix` `Matrix.semiring` `Pi.addCommMonoid` `Matrix.Module.matrixModule`	—	`ext` `RingHomCompTriple.ids`
`mapMatrixModule_comp_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Matrix` `Matrix.semiring` `Ring.toSemiring` `RingHom.id` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Matrix.Module.matrixModule` `instFunLike` `mapMatrixModule` `comp` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `mapMatrixModule_comp`
`mapMatrixModule_id` 📖	mathematical	—	`mapMatrixModule` `id` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Matrix` `Matrix.semiring` `Pi.addCommMonoid` `Matrix.Module.matrixModule`	—	`ext`
`mapMatrixModule_id_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Matrix` `Matrix.semiring` `Ring.toSemiring` `RingHom.id` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Matrix.Module.matrixModule` `instFunLike` `mapMatrixModule` `id`	—	`mapMatrixModule_id`

Matrix.Module

Definitions

Name	Category	Theorems
`matrixModule` 📖	CompOp	16 math math: `ModuleCat.toMatrixModCat_map`, `smul_def`, `LinearMap.mapMatrixModule_apply`, `LinearMap.mapMatrixModule_id_apply`, `instIsScalarTowerForall`, `scalar_smul`, `smul_apply`, `LinearMap.mapMatrixModule_comp`, `single_smul`, `LinearMap.mapMatrixModule_id`, `diagonal_const_smul`, `fromModuleCatToModuleCatLinearEquiv_apply`, `fromModuleCatToModuleCatLinearEquiv_symm_apply_coe`, `smul_def'`, `LinearMap.mapMatrixModule_comp_apply`, `ModuleCat.toMatrixModCat_obj_isModule`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diagonal_const_smul` 📖	mathematical	—	`Matrix` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring` `Pi.addMonoid` `Module.toDistribMulAction` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `matrixModule` `Matrix.diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Function.hasSMul`	—	`Finset.sum_congr` `ite_smul` `zero_smul` `Finset.sum_ite_eq`
`instIsScalarTowerForall` 📖	mathematical	—	`IsScalarTower` `Matrix` `Matrix.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring` `Pi.addMonoid` `Module.toDistribMulAction` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `matrixModule` `Function.hasSMul`	—	`Finset.sum_congr` `smul_assoc` `Finset.smul_sum`
`scalar_smul` 📖	mathematical	—	`Matrix` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring` `Pi.addMonoid` `Module.toDistribMulAction` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `matrixModule` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Matrix.nonAssocSemiring` `RingHom.instFunLike` `Matrix.scalar` `Function.hasSMul`	—	`diagonal_const_smul`
`single_smul` 📖	mathematical	—	`Matrix` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring` `Pi.addMonoid` `Module.toDistribMulAction` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `matrixModule` `Matrix.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Pi.single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Fintype.sum_eq_single` `Matrix.single_apply_of_ne` `zero_smul` `eq_or_ne` `Matrix.single_apply_same` `Pi.single_eq_same` `Pi.single_eq_of_ne'`
`smul_apply` 📖	mathematical	—	`Matrix` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring` `Pi.addMonoid` `Module.toDistribMulAction` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `matrixModule` `Finset.sum` `Finset.univ`	—	—
`smul_def` 📖	mathematical	—	`Matrix` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring` `Pi.addMonoid` `Module.toDistribMulAction` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `matrixModule` `Finset.sum` `Finset.univ`	—	—
`smul_def'` 📖	mathematical	—	`Matrix` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring` `Pi.addMonoid` `Module.toDistribMulAction` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `matrixModule` `Finset.sum` `Finset.univ`	—	`Finset.sum_apply`

---

← Back to Index