TheoremsaddProjection_respects_measure', covolume_ne_top, isFiniteMeasure_quotient, sigmaFiniteQuotient, unique, ExistsIsAddFundamentalDomain, ExistsIsFundamentalDomain, addProjection_respects_measure, addProjection_respects_measure_apply, addQuotientMeasureEqMeasurePreimage, addQuotientMeasureEqMeasurePreimage_addQuotientMeasure, addQuotientMeasureEqMeasurePreimage_of_zero, addQuotientMeasure_eq, ae_covers, aedisjoint, aestronglyMeasurable_on_iff, covolume_eq_volume, essSup_measure_restrict, exists_ne_zero_vadd_eq, hasAddFundamentalDomain, hasFiniteIntegral_on_iff, iUnion_vadd_ae_eq, image_of_equiv, integrableOn_iff, integral_eq_tsum, integral_eq_tsum', integral_eq_tsum'', integral_eq_tsum_of_ac, lintegral_eq_tsum, lintegral_eq_tsum', lintegral_eq_tsum'', lintegral_eq_tsum_of_ac, measurePreserving_add_quotient_mk, measure_addFundamentalFrontier, measure_addFundamentalInterior, measure_eq, measure_eq_card_smul_of_vadd_ae_eq_self, measure_eq_tsum, measure_eq_tsum', measure_eq_tsum_of_ac, measure_le_of_pairwise_disjoint, measure_ne_zero, measure_set_eq, measure_zero_of_invariant, mk', mk'', mk_of_measure_univ_le, mono, nullMeasurableSet, nullMeasurableSet_vadd, pairwise_aedisjoint_of_ac, preimage_of_equiv, restrict_restrict, setIntegral_eq, setIntegral_eq_tsum, setIntegral_eq_tsum', setLIntegral_eq, setLIntegral_eq_tsum, setLIntegral_eq_tsum', sum_restrict, sum_restrict_of_ac, vadd, vadd_of_comm, ae_covers, aedisjoint, aestronglyMeasurable_on_iff, covolume_eq_volume, essSup_measure_restrict, exists_ne_one_smul_eq, fundamentalInterior, hasFiniteIntegral_on_iff, hasFundamentalDomain, iUnion_smul_ae_eq, image_of_equiv, integrableOn_iff, integral_eq_tsum, integral_eq_tsum', integral_eq_tsum'', integral_eq_tsum_of_ac, lintegral_eq_tsum, lintegral_eq_tsum', lintegral_eq_tsum'', lintegral_eq_tsum_of_ac, measurePreserving_quotient_mk, measure_eq, measure_eq_card_smul_of_smul_ae_eq_self, measure_eq_tsum, measure_eq_tsum', measure_eq_tsum_of_ac, measure_fundamentalFrontier, measure_fundamentalInterior, measure_le_of_pairwise_disjoint, measure_ne_zero, measure_set_eq, measure_zero_of_invariant, mk', mk'', mk_of_measure_univ_le, mono, nullMeasurableSet, nullMeasurableSet_smul, pairwise_aedisjoint_of_ac, preimage_of_equiv, projection_respects_measure, projection_respects_measure_apply, quotientMeasureEqMeasurePreimage, quotientMeasureEqMeasurePreimage_of_zero, quotientMeasureEqMeasurePreimage_quotientMeasure, quotientMeasure_eq, restrict_restrict, setIntegral_eq, setIntegral_eq_tsum, setIntegral_eq_tsum', setLIntegral_eq, setLIntegral_eq_tsum, setLIntegral_eq_tsum', smul, smul_of_comm, sum_restrict, sum_restrict_of_ac, addFundamentalFrontier, addFundamentalInterior, fundamentalFrontier, fundamentalInterior, covolume_ne_top, isFiniteMeasure_quotient, projection_respects_measure', sigmaFiniteQuotient, unique, addFundamentalFrontier_subset, addFundamentalFrontier_union_addFundamentalInterior, addFundamentalFrontier_vadd, addFundamentalInterior_subset, addFundamentalInterior_union_addFundamentalFrontier, addFundamentalInterior_vadd, addMeasure_map_restrict_apply, disjoint_addFundamentalInterior_addFundamentalFrontier, disjoint_fundamentalInterior_fundamentalFrontier, fundamentalFrontier_smul, fundamentalFrontier_subset, fundamentalFrontier_union_fundamentalInterior, fundamentalInterior_smul, fundamentalInterior_subset, fundamentalInterior_union_fundamentalFrontier, instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace, instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume, measure_map_restrict_apply, mem_addFundamentalFrontier, mem_addFundamentalInterior, mem_fundamentalFrontier, mem_fundamentalInterior, pairwise_disjoint_addFundamentalInterior, pairwise_disjoint_fundamentalInterior, sdiff_addFundamentalFrontier, sdiff_addFundamentalInterior, sdiff_fundamentalFrontier, sdiff_fundamentalInterior | 157 |