Algebra

📁 Source: Mathlib/Algebra/Category/ModuleCat/Algebra.lean

Statistics

Metric	Count
Definitions linearOverField, moduleOfAlgebraModule	2
Theorems isScalarTower_of_algebra_moduleCat	1
Total	3

ModuleCat

Definitions

Name	Category	Theorems
linearOverField 📖	CompOp	—
moduleOfAlgebraModule 📖	CompOp	1 math math: isScalarTower_of_algebra_moduleCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isScalarTower_of_algebra_moduleCat 📖	mathematical	—	IsScalarTower carrier Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Ring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup isAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid isModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring moduleOfAlgebraModule	—	RestrictScalars.isScalarTower

---

← Back to Index