Quotient.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

30 declarations, 0 contain sorry, 0 declared as axioms

Relation between the quotient haar measure and the measure on the whole group.

Let G be a second countable locally compact topological group, and N be a closed normal subgroup of G. Given haar measures dn on N and d𝓍 on G ⧸ N, we can define a measure dg on G via ∫ f(x) dx = ∫ (∫ f(xn) dn) d𝓍. We show that this is a haar measure, and as a conclusion we can relate the modular character of G to the one of G / N.

Imports (2)

Imported by 2 files

lemma exists_continuous_and_indicator_le_of_isCompact line 27 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, T2Space, LocallyCompactSpace, Set, IsCompact, IsOpen, LE.le, Exists, Real, And, Continuous, HasCompactSupport, Set.indicator, OfNat.ofNat
Proof uses: interior, exists_compact_between, CompactSpace, Membership.mem, Iff.mp, isCompact_iff_compactSpace, ContinuousMap, Set.EqOn, Set.preimage, Subtype, Compl.compl, Set.Icc, exists_continuous_zero_one_of_isClosed, IsClosed.preimage, continuous_subtype_val, IsOpen.isClosed_compl, isOpen_interior, IsCompact.isClosed, Iff.mpr, Disjoint and 69 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
lemma exists_continuous_nnreal_and_indicator_le_of_isCompact line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, T2Space, LocallyCompactSpace, Set, IsCompact, IsOpen, LE.le, Exists, NNReal, And, Continuous, HasCompactSupport, Set.indicator, OfNat.ofNat
Proof uses: Real, exists_continuous_and_indicator_le_of_isCompact, Eq, Function.comp, Exists.intro, Subtype.mk, LE.le.trans, Set.indicator_nonneg, of_eq_true, Membership.mem, Eq.trans, True, forall_congr, implies_congr, Eq.refl, implies_true, rfl, And.intro, Iff.mpr, Topology.IsEmbedding.continuous_iff and 21 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.setLIntegral_lt_top_of_isCompact_of_ne_top line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, Set, Ne, ENNReal, Top.top, IsCompact, Continuous, LT.lt, MeasureTheory.lintegral, MeasureTheory.Measure.restrict
Proof uses: NNReal, Eq, Function.comp, Exists, Exists.intro, ENNReal.toNNReal, funext, of_eq_true, Eq.trans, True, congrArg, ENNReal.coe_toNNReal, Not, False, eq_false, not_false_eq_true, eq_self, MeasureTheory.setLIntegral_lt_top_of_isCompact, Iff.mpr, Topology.IsEmbedding.continuous_iff and 2 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Set.inv_smul_set_eq_preimage_mul line 90 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Set, Eq, HSMul.hSMul, Inv.inv, Set.preimage, HMul.hMul
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, True, congr, congrArg, congrFun', inv_inv, iff_self
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance (instance at line 93) line 93 source
instance (instance at line 98) line 98 source
def MeasureTheory.Measure.ofQuotientIntegrand line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MeasurableSpace, Subgroup, MeasureTheory.Measure, Subtype, Membership.mem, MeasurableMul₂, MeasureTheory.Measure.IsMulLeftInvariant, ENNReal, HasQuotient.Quotient
Proof uses: Quotient.lift, QuotientGroup.leftRel, MeasureTheory.lintegral, HMul.hMul, HasEquiv.Equiv
24 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Measure.ofQuotientIntegrand_mk line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MeasurableSpace, Subgroup, MeasureTheory.Measure, Subtype, Membership.mem, MeasurableMul₂, MeasureTheory.Measure.IsMulLeftInvariant, ENNReal, Eq, MeasureTheory.Measure.ofQuotientIntegrand, MeasureTheory.lintegral, HMul.hMul
Proof uses: rfl
22 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.Measure.ofQuotientIntegrand_indicator line 123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MeasurableSpace, Subgroup, MeasureTheory.Measure, Subtype, Membership.mem, MeasurableMul₂, MeasureTheory.Measure.IsMulLeftInvariant, Set, MeasurableSet, Eq, ENNReal, MeasureTheory.Measure.ofQuotientIntegrand, Set.indicator, OfNat.ofNat, Set.preimage, HSMul.hSMul, Inv.inv
Proof uses: id, Eq.mpr, MeasureTheory.lintegral, HMul.hMul, congrArg, Eq.symm, MeasureTheory.lintegral_indicator_one, MeasurableSet.preimage, MeasurableSet.const_smul, measurable_subtype_coe, Eq.rec, Eq.refl, funext, Decidable, ite, Subsingleton.elim, of_eq_true, Eq.trans, True, eq_self and 1 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.(instance at line 132) line 132 source
instance MeasureTheory.(instance at line 138) line 138 source
instance MeasureTheory.(instance at line 142) line 142 source
instance MeasureTheory.(instance at line 145) line 145 source
lemma MeasureTheory.Measure.ofQuotientIntegrand_indicator_mul_preimage line 154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, IsTopologicalGroup, SecondCountableTopology, LocallyCompactSpace, MeasurableSpace, BorelSpace, Subgroup, IsClosed, MeasureTheory.Measure, Subtype, Membership.mem, MeasureTheory.Measure.IsHaarMeasure, Set, MeasurableSet, HasQuotient.Quotient, Subgroup.Normal, Eq, ENNReal, MeasureTheory.Measure.ofQuotientIntegrand and 9 more
Proof uses: Exists, QuotientGroup.mk_surjective, Eq.mpr, HSMul.hSMul, Inv.inv, id, congrArg, MeasureTheory.Measure.ofQuotientIntegrand_indicator, MeasurableSet.preimage, Measurable.mul_const, measurable_id', Eq.symm, QuotientGroup.mk_mul, NNReal, MeasureTheory.Measure.map, ContinuousMulEquiv, Eq.rec, Eq.refl, Eq.trans, MeasureTheory.mulEquivHaarChar_smul_map and 24 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Measure.ofQuotientIntegrand_zero line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MeasurableSpace, Subgroup, MeasureTheory.Measure, Subtype, Membership.mem, MeasurableMul₂, MeasureTheory.Measure.IsMulLeftInvariant, HasQuotient.Quotient, Eq, ENNReal, MeasureTheory.Measure.ofQuotientIntegrand, OfNat.ofNat
Proof uses: Exists, QuotientGroup.mk_surjective, of_eq_true, Eq.trans, True, congrFun', congrArg, MeasureTheory.lintegral, HMul.hMul, Set, Set.univ, MeasureTheory.lintegral_const, MulZeroClass.zero_mul, eq_self
38 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Measure.ofQuotientIntegrand_fun_zero line 184 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MeasurableSpace, Subgroup, MeasureTheory.Measure, Subtype, Membership.mem, MeasurableMul₂, MeasureTheory.Measure.IsMulLeftInvariant, HasQuotient.Quotient, Eq, ENNReal, MeasureTheory.Measure.ofQuotientIntegrand, OfNat.ofNat
Proof uses: MeasureTheory.Measure.ofQuotientIntegrand_zero
22 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.Measure.ofQuotientIntegrand_mono line 188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MeasurableSpace, Subgroup, MeasureTheory.Measure, Subtype, Membership.mem, MeasurableMul₂, MeasureTheory.Measure.IsMulLeftInvariant, ENNReal, LE.le, HasQuotient.Quotient, MeasureTheory.Measure.ofQuotientIntegrand
Proof uses: Eq, Exists, QuotientGroup.mk_surjective, MeasureTheory.lintegral_mono, HMul.hMul
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Measure.ofQuotientIntegrand_iUnion line 193 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MeasurableSpace, Subgroup, MeasureTheory.Measure, Subtype, Membership.mem, MeasurableMul₂, MeasureTheory.Measure.IsMulLeftInvariant, Countable, Set, MeasurableSet, Pairwise, Function.onFun, Disjoint, HasQuotient.Quotient, Eq, ENNReal, MeasureTheory.Measure.ofQuotientIntegrand, Set.indicator, Set.iUnion and 3 more
Proof uses: Exists, QuotientGroup.mk_surjective, Eq.mpr, Set.preimage, HSMul.hSMul, Inv.inv, id, congr, congrArg, MeasureTheory.Measure.ofQuotientIntegrand_indicator, MeasurableSet.iUnion, congrFun', SummationFilter, optParam, funext, of_eq_true, eq_true, Set.smul_set_iUnion, Set.preimage_iUnion, MeasureTheory.measure_iUnion and 16 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Measure.measurable_ofQuotientIntegrand line 208 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MeasurableSpace, Subgroup, MeasureTheory.Measure, Subtype, Membership.mem, MeasurableMul₂, MeasureTheory.Measure.IsMulLeftInvariant, MeasureTheory.SFinite, ENNReal, Measurable, HasQuotient.Quotient, MeasureTheory.Measure.ofQuotientIntegrand
Proof uses: Iff.mpr, Quotient, QuotientGroup.leftRel, Function.comp, Quotient.mk'', measurable_from_quotient, Measurable.lintegral_prod_right, HMul.hMul, Measurable.comp, Prod, Prod.fst, Prod.snd, Prod.map, id, MeasurableMul₂.measurable_mul, Measurable.prodMap, measurable_id, measurable_subtype_coe
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.Measure.ofQuotient line 222 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MeasurableSpace, Subgroup, MeasureTheory.Measure, HasQuotient.Quotient, Subtype, Membership.mem, MeasurableMul₂, MeasureTheory.Measure.IsMulLeftInvariant, MeasureTheory.SFinite
Proof uses: MeasureTheory.Measure.ofMeasurable, Set, MeasurableSet, MeasureTheory.lintegral, MeasureTheory.Measure.ofQuotientIntegrand, Set.indicator, ENNReal, OfNat.ofNat, Nat, Pairwise, Function.onFun, Disjoint
37 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Measure.ofQuotient_apply line 229 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MeasurableSpace, Subgroup, MeasureTheory.Measure, HasQuotient.Quotient, Subtype, Membership.mem, MeasurableMul₂, MeasureTheory.Measure.IsMulLeftInvariant, MeasureTheory.SFinite, Set, MeasurableSet, Eq, ENNReal, MeasureTheory.Measure.ofQuotient, MeasureTheory.lintegral, MeasureTheory.Measure.ofQuotientIntegrand, Set.indicator, OfNat.ofNat
Proof uses: MeasureTheory.Measure.ofMeasurable_apply, Nat, Pairwise, Function.onFun, Disjoint
43 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.(instance at line 233) line 233 source
instance MeasureTheory.(instance at line 242) line 242 source
lemma MeasureTheory.Measure.continuous_ofQuotientIntegrand line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MeasurableSpace, Subgroup, MeasureTheory.Measure, Subtype, Membership.mem, TopologicalSpace, OpensMeasurableSpace, IsTopologicalGroup, WeaklyLocallyCompactSpace, MeasurableMul₂, MeasureTheory.Measure.IsMulLeftInvariant, MeasureTheory.IsFiniteMeasureOnCompacts, IsClosed, NNReal, Continuous, HasCompactSupport, HasQuotient.Quotient, ENNReal, MeasureTheory.Measure.ofQuotientIntegrand
Proof uses: Iff.mpr, TopologicalSpace.coinduced, Function.comp, continuous_coinduced_dom, id, MeasureTheory.Integrable, Real, HMul.hMul, Continuous.integrable_of_hasCompactSupport, Set, Continuous.comp', NNReal.continuous_coe, Continuous.const_mul, continuous_subtype_val, Iff.mp, Exists, And, IsCompact, Not, Eq and 59 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Measure.ofQuotientIntegrand_lt_top line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MeasurableSpace, Subgroup, MeasureTheory.Measure, Subtype, Membership.mem, TopologicalSpace, IsTopologicalGroup, MeasurableMul₂, MeasureTheory.Measure.IsMulLeftInvariant, MeasureTheory.IsFiniteMeasureOnCompacts, IsClosed, NNReal, Continuous, HasCompactSupport, HasQuotient.Quotient, LT.lt, ENNReal, MeasureTheory.Measure.ofQuotientIntegrand, Top.top
Proof uses: Eq, Exists, QuotientGroup.mk_surjective, id, Eq.mpr, MeasureTheory.lintegral, HMul.hMul, MeasureTheory.Measure.restrict, Set.preimage, HSMul.hSMul, Set, Inv.inv, tsupport, congrArg, Eq.symm, MeasureTheory.setLIntegral_eq_of_support_subset, LE.le, Function.support, closure, tsupport.eq_1 and 23 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.(instance at line 304) line 304 source
instance MeasureTheory.(instance at line 330) line 330 source
instance MeasureTheory.(instance at line 343) line 343 source
lemma MeasureTheory.modularCharacter_eq_modularCharacter_quotient_mul_mulEquivHaarChar line 347 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, IsTopologicalGroup, MeasurableSpace, BorelSpace, LocallyCompactSpace, T2Space, SecondCountableTopology, Subgroup, Subgroup.Normal, IsClosed, Eq, NNReal, MonoidHom, MeasureTheory.Measure.modularCharacter, HMul.hMul, HasQuotient.Quotient, MeasureTheory.mulEquivHaarChar, Subtype, Membership.mem and 4 more
Proof uses: PolishSpace, polish_of_locally_compact_second_countable, Topology.IsClosedEmbedding.locallyCompactSpace, Set, IsClosed.isClosedEmbedding_subtypeVal, TopologicalSpace.PositiveCompacts, LE.le, Set.univ, Exists, exists_positiveCompacts_subset, isOpen_univ, of_eq_true, Set.Nonempty, ENNReal, MeasureTheory.Measure, MeasureTheory.Measure.map, MeasureTheory.Measure.ofQuotient, MeasureTheory.Measure.haar, Classical.arbitrary, HSMul.hSMul and 75 more
176 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory._root_.QuotientGroup.isUnimodularGroup The quotient of a Hausdorff second countable unimodular group by a central normal closed subgroup is still unimodular line 383 source
Source documentation
The quotient of a Hausdorff second countable unimodular group by a central normal closed subgroup is still unimodular.
```
lemma _root_.QuotientGroup.isUnimodularGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsUnimodularGroup G]
    [T2Space G] [SecondCountableTopology G] (N : Subgroup G) [N.Normal]
    (hN : N ≤ .center G) (hN' : IsClosed (X := G) N) : IsUnimodularGroup (G ⧸ N) where
…
```
Mentions: IsUnimodularGroup