Measurability on the quotient of a module by a submodule

instance Submodule.Quotient.instMeasurableSpaceQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p : Submodule R M} [MeasurableSpace M] : MeasurableSpace (M ⧸ p)

Equations

• Submodule.Quotient.instMeasurableSpaceQuotient = Quotient.instMeasurableSpace

instance Submodule.Quotient.instDiscreteMeasurableSpaceQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p : Submodule R M} [MeasurableSpace M] [DiscreteMeasurableSpace M] : DiscreteMeasurableSpace (M ⧸ p)