Documentation Verification Report

DirectLimit

📁 Source: Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean

Statistics

Metric	Count
Definitions `directLimitLeft`, `directLimitRight`, `fromDirectLimit`, `toDirectLimit`	4
Theorems `directLimitLeft_rTensor_of`, `directLimitLeft_symm_of_tmul`, `directLimitLeft_tmul_of`, `directLimitRight_symm_of_tmul`, `directLimitRight_tmul_of`, `fromDirectLimit_of_tmul`, `instDirectedSystemCoeLinearMapIdLTensor`, `instDirectedSystemCoeLinearMapIdRTensor`, `toDirectLimit_tmul_of`	9
Total	13

TensorProduct

Definitions

Name	Category	Theorems
`directLimitLeft` 📖	CompOp	3 math math: `directLimitLeft_rTensor_of`, `directLimitLeft_tmul_of`, `directLimitLeft_symm_of_tmul`
`directLimitRight` 📖	CompOp	2 math math: `directLimitRight_tmul_of`, `directLimitRight_symm_of_tmul`
`fromDirectLimit` 📖	CompOp	1 math math: `fromDirectLimit_of_tmul`
`toDirectLimit` 📖	CompOp	1 math math: `toDirectLimit_tmul_of`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directLimitLeft_rTensor_of` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `Module.DirectLimit` `Module.DirectLimit.addCommMonoid` `Module.DirectLimit.module` `addCommMonoid` `instModule` `LinearMap.rTensor` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `directLimitLeft` `LinearMap` `LinearMap.instFunLike` `Module.DirectLimit.of`	—	`induction_on` `RingHomInvPair.ids` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `directLimitLeft_tmul_of` `map_add` `SemilinearMapClass.toAddHomClass`
`directLimitLeft_symm_of_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.DirectLimit` `TensorProduct` `addCommMonoid` `instModule` `LinearMap.rTensor` `Module.DirectLimit.addCommMonoid` `Module.DirectLimit.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `directLimitLeft` `LinearMap` `LinearMap.instFunLike` `Module.DirectLimit.of` `tmul`	—	`fromDirectLimit_of_tmul`
`directLimitLeft_tmul_of` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `Module.DirectLimit` `Module.DirectLimit.addCommMonoid` `Module.DirectLimit.module` `addCommMonoid` `instModule` `LinearMap.rTensor` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `directLimitLeft` `tmul` `LinearMap` `LinearMap.instFunLike` `Module.DirectLimit.of`	—	`toDirectLimit_tmul_of`
`directLimitRight_symm_of_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.DirectLimit` `TensorProduct` `addCommMonoid` `instModule` `LinearMap.lTensor` `Module.DirectLimit.addCommMonoid` `Module.DirectLimit.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `directLimitRight` `LinearMap` `LinearMap.instFunLike` `Module.DirectLimit.of` `tmul`	—	`RingHomInvPair.ids` `Module.DirectLimit.congr_symm_apply_of` `directLimitLeft_symm_of_tmul`
`directLimitRight_tmul_of` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `Module.DirectLimit` `Module.DirectLimit.addCommMonoid` `Module.DirectLimit.module` `addCommMonoid` `instModule` `LinearMap.lTensor` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `directLimitRight` `tmul` `LinearMap` `LinearMap.instFunLike` `Module.DirectLimit.of`	—	`RingHomInvPair.ids` `directLimitLeft_tmul_of` `Module.DirectLimit.congr_apply_of`
`fromDirectLimit_of_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.DirectLimit` `TensorProduct` `addCommMonoid` `instModule` `LinearMap.rTensor` `Module.DirectLimit.addCommMonoid` `Module.DirectLimit.module` `LinearMap.instFunLike` `fromDirectLimit` `Module.DirectLimit.of` `tmul`	—	`Module.DirectLimit.lift_of`
`instDirectedSystemCoeLinearMapIdLTensor` 📖	mathematical	—	`DirectedSystem` `TensorProduct` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `LinearMap.instFunLike` `LinearMap.lTensor`	—	`le_rfl` `LinearMap.ext` `DirectedSystem.map_self'` `LinearMap.lTensor_id_apply` `RingHomCompTriple.ids` `LE.le.trans` `DirectedSystem.map_map'` `LinearMap.lTensor_comp_apply`
`instDirectedSystemCoeLinearMapIdRTensor` 📖	mathematical	—	`DirectedSystem` `TensorProduct` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `LinearMap.instFunLike` `LinearMap.rTensor`	—	`le_rfl` `LinearMap.ext` `DirectedSystem.map_self'` `LinearMap.rTensor_id_apply` `RingHomCompTriple.ids` `LE.le.trans` `DirectedSystem.map_map'` `LinearMap.rTensor_comp_apply`
`toDirectLimit_tmul_of` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `Module.DirectLimit` `Module.DirectLimit.addCommMonoid` `Module.DirectLimit.module` `addCommMonoid` `instModule` `LinearMap.rTensor` `LinearMap.instFunLike` `toDirectLimit` `tmul` `Module.DirectLimit.of`	—	`toDirectLimit.eq_1` `smulCommClass_self` `lift.tmul` `Module.DirectLimit.lift_of`

---

← Back to Index