SubmoduleQuotient

📁 Source: Mathlib/MeasureTheory/Constructions/SubmoduleQuotient.lean

Statistics

Metric	Count
Definitions instMeasurableSpaceQuotient	1
Theorems instDiscreteMeasurableSpaceQuotient	1
Total	2

Submodule.Quotient

Definitions

Name	Category	Theorems
instMeasurableSpaceQuotient 📖	CompOp	1 math math: instDiscreteMeasurableSpaceQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteMeasurableSpaceQuotient 📖	mathematical	—	DiscreteMeasurableSpace HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient instMeasurableSpaceQuotient	—	Quotient.instDiscreteMeasurableSpace

---

← Back to Index