Documentation Verification Report

WithAlgebraicStructures

📁 Source: Mathlib/CategoryTheory/Limits/ConcreteCategory/WithAlgebraicStructures.lean

Statistics

Metric	Count
Definitions	0
Theorems `colimit_no_zero_smul_divisor`, `colimit_rep_eq_zero`	2
Total	2

CategoryTheory.Limits.Concrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`colimit_no_zero_smul_divisor` 📖	—	`ModuleCat.carrier` `CategoryTheory.Functor.obj` `ModuleCat` `ModuleCat.moduleCategory` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `ModuleCat.isAddCommGroup` `CategoryTheory.ToType` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Limits.colimit` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—	`colimit_exists_rep` `colimit_rep_eq_zero` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `CategoryTheory.comp_apply` `Mathlib.Tactic.Elementwise.hom_elementwise` `CategoryTheory.Limits.colimit.w` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `CategoryTheory.IsFiltered.toSup_commutes` `CategoryTheory.Functor.map_comp` `ModuleCat.comp_apply`
`colimit_rep_eq_zero` 📖	mathematical	`DFunLike.coe` `CategoryTheory.Functor.obj` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.Limits.colimit` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.Limits.colimit.ι` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`ModuleCat.Hom.hom` `CategoryTheory.Functor.map`	—	`colimit_rep_eq_iff_exists` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`

---

← Back to Index