Documentation Verification Report

Category

📁 Source: Mathlib/RingTheory/Regular/Category.lean

Statistics

Metric	Count
Definitions `smulShortComplex`	1
Theorems `smulShortComplex_shortExact`, `exact_smul_id_smul_top_mkQ`, `smulShortComplex_X₁`, `smulShortComplex_X₂`, `smulShortComplex_X₃_carrier`, `smulShortComplex_X₃_isAddCommGroup`, `smulShortComplex_X₃_isModule`, `smulShortComplex_exact`, `smulShortComplex_f`, `smulShortComplex_g`, `smulShortComplex_g_epi`	11
Total	12

IsSMulRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smulShortComplex_shortExact` 📖	mathematical	`IsSMulRegular` `ModuleCat.carrier` `CommRing.toRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `ModuleCat.isAddCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `ModuleCat.isModule`	`CategoryTheory.ShortComplex.ShortExact` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive` `ModuleCat.smulShortComplex`	—	`ModuleCat.smulShortComplex_exact` `ModuleCat.smulShortComplex_g_epi`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact_smul_id_smul_top_mkQ` 📖	mathematical	—	`Function.Exact` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submodule.pointwiseDistribMulAction` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Top.top` `Submodule.instTop` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `instSMul` `id` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.mkQ` `Submodule.Quotient.instZeroQuotient`	—	`smulCommClass_self`

ModuleCat

Definitions

Name	Category	Theorems
`smulShortComplex` 📖	CompOp	10 math math: `smulShortComplex_X₃_isAddCommGroup`, `smulShortComplex_X₁`, `smulShortComplex_g`, `smulShortComplex_X₃_carrier`, `smulShortComplex_f`, `IsSMulRegular.smulShortComplex_shortExact`, `smulShortComplex_X₃_isModule`, `smulShortComplex_X₂`, `smulShortComplex_g_epi`, `smulShortComplex_exact`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smulShortComplex_X₁` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₁` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `smulShortComplex`	—	—
`smulShortComplex_X₂` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₂` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `smulShortComplex`	—	—
`smulShortComplex_X₃_carrier` 📖	mathematical	—	`carrier` `CommRing.toRing` `CategoryTheory.ShortComplex.X₃` `ModuleCat` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `smulShortComplex` `QuotSMulTop` `isAddCommGroup` `isModule`	—	—
`smulShortComplex_X₃_isAddCommGroup` 📖	mathematical	—	`isAddCommGroup` `CommRing.toRing` `CategoryTheory.ShortComplex.X₃` `ModuleCat` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `smulShortComplex` `Submodule.Quotient.addCommGroup` `carrier` `isModule` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submodule.pointwiseDistribMulAction` `Module.toDistribMulAction` `Top.top` `Submodule.instTop`	—	—
`smulShortComplex_X₃_isModule` 📖	mathematical	—	`isModule` `CommRing.toRing` `CategoryTheory.ShortComplex.X₃` `ModuleCat` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `smulShortComplex` `Submodule.Quotient.module` `carrier` `isAddCommGroup` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submodule.pointwiseDistribMulAction` `Module.toDistribMulAction` `Top.top` `Submodule.instTop`	—	—
`smulShortComplex_exact` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `smulShortComplex`	—	—
`smulShortComplex_f` 📖	mathematical	—	`CategoryTheory.ShortComplex.f` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `smulShortComplex` `ofHom` `carrier` `isAddCommGroup` `isModule` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.id`	—	—
`smulShortComplex_g` 📖	mathematical	—	`CategoryTheory.ShortComplex.g` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `smulShortComplex` `ofHom` `carrier` `QuotSMulTop` `isAddCommGroup` `isModule` `Submodule.Quotient.addCommGroup` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submodule.pointwiseDistribMulAction` `Module.toDistribMulAction` `Top.top` `Submodule.instTop` `Submodule.Quotient.module` `Submodule.mkQ`	—	—
`smulShortComplex_g_epi` 📖	mathematical	—	`CategoryTheory.Epi` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `smulShortComplex` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g`	—	`Submodule.mkQ_surjective`

---

← Back to Index