Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Module/LinearMap/Basic.lean

Statistics

Metric	Count
Definitions `instDistribMulActionDomMulActOfSMulCommClass`, `instModuleDomMulActOfSMulCommClass`, `instSMulDomMulAct`, `ltoFun`, `elimZeroLeft`, `elimZeroRight`	6
Theorems `coe_smul_linearMap`, `mk_smul_linearMap_apply`, `smul_linearMap_apply`, `instIsTorsionFree`, `instSMulCommClassDomMulAct`, `ltoFun_apply`, `mulLeft_eq_zero_iff`, `mulLeft_inj`, `mulLeft_mul`, `mulLeft_one`, `mulRight_eq_zero_iff`, `mulRight_inj`, `mulRight_mul`, `mulRight_one`, `elimZeroLeft_apply`, `elimZeroRight_apply`	16
Total	22

DomMulAct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_smul_linearMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `DomMulAct` `LinearMap.instSMulDomMulAct` `instSMulForall` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—
`mk_smul_linearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `DomMulAct` `LinearMap.instSMulDomMulAct` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—
`smul_linearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `DomMulAct` `LinearMap.instSMulDomMulAct` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—

LinearMap

Definitions

Name	Category	Theorems
`instDistribMulActionDomMulActOfSMulCommClass` 📖	CompOp	—
`instModuleDomMulActOfSMulCommClass` 📖	CompOp	2 math math: `LinearEquiv.domMulActCongrRight_symm_apply`, `LinearEquiv.domMulActCongrRight_apply`
`instSMulDomMulAct` 📖	CompOp	4 math math: `DomMulAct.smul_linearMap_apply`, `DomMulAct.coe_smul_linearMap`, `DomMulAct.mk_smul_linearMap_apply`, `instSMulCommClassDomMulAct`
`ltoFun` 📖	CompOp	1 math math: `ltoFun_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTorsionFree` 📖	mathematical	—	`Module.IsTorsionFree` `LinearMap` `addCommMonoid` `module`	—	`Function.Injective.moduleIsTorsionFree` `Pi.instModuleIsTorsionFree` `coe_injective` `coe_smul`
`instSMulCommClassDomMulAct` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `LinearMap` `instSMulDomMulAct`	—	`ext` `SMulCommClass.smul_comm`
`ltoFun_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `Pi.addCommMonoid` `module` `Pi.Function.module` `instFunLike` `ltoFun`	—	—
`mulLeft_eq_zero_iff` 📖	mathematical	—	`mulLeft` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`mulLeft_zero_eq_zero`
`mulLeft_inj` 📖	mathematical	—	`mulLeft` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`mul_one` `ext_iff`
`mulLeft_mul` 📖	mathematical	—	`mulLeft` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `comp` `NonUnitalNonAssocSemiring.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`ext` `RingHomCompTriple.ids` `mul_assoc`
`mulLeft_one` 📖	mathematical	—	`mulLeft` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `id` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`ext` `one_mul`
`mulRight_eq_zero_iff` 📖	mathematical	—	`mulRight` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`mulRight_zero_eq_zero`
`mulRight_inj` 📖	mathematical	—	`mulRight` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`one_mul` `ext_iff`
`mulRight_mul` 📖	mathematical	—	`mulRight` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `comp` `NonUnitalNonAssocSemiring.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`ext` `RingHomCompTriple.ids` `mul_assoc`
`mulRight_one` 📖	mathematical	—	`mulRight` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `id` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`ext` `mul_one`

Sum

Definitions

Name	Category	Theorems
`elimZeroLeft` 📖	CompOp	1 math math: `elimZeroLeft_apply`
`elimZeroRight` 📖	CompOp	1 math math: `elimZeroRight_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elimZeroLeft_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `elimZeroLeft` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`elimZeroRight_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `elimZeroRight` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—

---

← Back to Index