Mod_

📁 Source: Mathlib/CategoryTheory/Monoidal/Cartesian/Mod_.lean

Statistics

Metric	Count
Definitions trivialAction, trivialAction, trivialAction	3
Theorems trivialAction_X, trivialAction_mod_smul	2
Total	5

CategoryTheory.ModObj

Definitions

Name	Category	Theorems
trivialAction 📖	CompOp	—

CategoryTheory.Mod_

Definitions

Name	Category	Theorems
trivialAction 📖	CompOp	2 math math: trivialAction_X, trivialAction_mod_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trivialAction_X 📖	mathematical	—	X CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategory.selfLeftAction CategoryTheory.Mon.X CategoryTheory.Mon.mon trivialAction	—	—
trivialAction_mod_smul 📖	mathematical	—	CategoryTheory.ModObj.smul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategory.selfLeftAction CategoryTheory.Mon.X CategoryTheory.Mon.mon mod trivialAction CategoryTheory.SemiCartesianMonoidalCategory.snd	—	—

CategoryTheory.Mod_Class

Definitions

Name	Category	Theorems
trivialAction 📖	CompOp	—

---

← Back to Index