Documentation

Mathlib.MeasureTheory.Constructions.SubmoduleQuotient

Measurability on the quotient of a module by a submodule #

source
🔸 coverage
@[implicit_reducible]
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)
source
📐 coverage
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)