Defs

📁 Source: Mathlib/Algebra/Module/Congruence/Defs.lean

Statistics

Metric	Count
Definitions ModuleCon, instAddCommGroupQuotient, instAddCommMagmaQuotient, instAddCommMonoidQuotient, instAddCommSemigroupQuotient, instAddGroupQuotient, instAddMonoidQuotient, instAddQuotient, instAddSemigroupQuotient, instAddZeroClassQuotient, instDistribMulActionQuotient, instDistribSMulQuotient, instModuleQuotient, instMulActionQuotient, instSMulQuotient, instSMulWithZeroQuotient, instSMulZeroClassQuotient, instZeroQuotient, ker, quotientKerEquivOfSurjective, toAddCon, toSMulCon, SMulCon, addConGen, addConGen', instMulActionQuotient, instSMulQuotient, instSMulWithZeroQuotient, instSMulZeroClassQuotient, instZeroQuotient, ker, toSetoid, VAddCon, instAddActionQuotient, instVAddQuotient, ker, toSetoid	37
Theorems smul, smul, vadd	3
Total	40

ModuleCon

Definitions

Name	Category	Theorems
instAddCommGroupQuotient 📖	CompOp	—
instAddCommMagmaQuotient 📖	CompOp	—
instAddCommMonoidQuotient 📖	CompOp	1 math math: instInvertibleReprₛ
instAddCommSemigroupQuotient 📖	CompOp	—
instAddGroupQuotient 📖	CompOp	—
instAddMonoidQuotient 📖	CompOp	—
instAddQuotient 📖	CompOp	—
instAddSemigroupQuotient 📖	CompOp	—
instAddZeroClassQuotient 📖	CompOp	—
instDistribMulActionQuotient 📖	CompOp	—
instDistribSMulQuotient 📖	CompOp	—
instModuleQuotient 📖	CompOp	1 math math: instInvertibleReprₛ
instMulActionQuotient 📖	CompOp	—
instSMulQuotient 📖	CompOp	—
instSMulWithZeroQuotient 📖	CompOp	—
instSMulZeroClassQuotient 📖	CompOp	—
instZeroQuotient 📖	CompOp	—
ker 📖	CompOp	—
quotientKerEquivOfSurjective 📖	CompOp	—
toAddCon 📖	CompOp	1 math math: Module.DirectLimit.quotMk_of
toSMulCon 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	—	AddCon.toSetoid toAddCon	—	—	—

SMulCon

Definitions

Name	Category	Theorems
addConGen 📖	CompOp	—
addConGen' 📖	CompOp	—
instMulActionQuotient 📖	CompOp	—
instSMulQuotient 📖	CompOp	—
instSMulWithZeroQuotient 📖	CompOp	—
instSMulZeroClassQuotient 📖	CompOp	—
instZeroQuotient 📖	CompOp	—
ker 📖	CompOp	—
toSetoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	—	toSetoid	—	—	—

VAddCon

Definitions

Name	Category	Theorems
instAddActionQuotient 📖	CompOp	—
instVAddQuotient 📖	CompOp	—
ker 📖	CompOp	—
toSetoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
vadd 📖	mathematical	toSetoid	HVAdd.hVAdd instHVAdd	—	—

(root)

Definitions

Name	Category	Theorems
ModuleCon 📖	CompData	—
SMulCon 📖	CompData	—
VAddCon 📖	CompData	—

---

← Back to Index