ModularCharacter.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

44 declarations, 0 contain sorry, 0 declared as axioms

Unimodular groups

We define unimodular groups, and show that [K₂ : gK₁g⁻¹] = [K₂ : K₁] for open compacts in unimodular groups.

We also show that GLₙ(K) is unimodular for K a second countable locally compact Hausdorff topological field.

Imports (10)

Imported by 3 files

lemma MeasureTheory.IsFiniteMeasureOnCompacts.withDensity line 35 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasureOnCompacts, OpensMeasurableSpace, T2Space, ENNReal, Continuous, LT.lt, Top.top, MeasureTheory.Measure.withDensity
Proof uses: MeasureTheory.IsFiniteMeasureOnCompacts.mk, Set, IsCompact, Eq.mpr, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, id, Eq, congrArg, MeasureTheory.withDensity_apply, IsCompact.measurableSet, EmptyCollection.emptyCollection, Set.Nonempty, Or, Set.eq_empty_or_nonempty, of_eq_true, Eq.trans, OfNat.ofNat, True, congrFun' and 21 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Measure.IsOpenPosMeasure.withDensity line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsOpenPosMeasure, LocallyCompactSpace, ENNReal, Continuous, Measurable, Ne, OfNat.ofNat, MeasureTheory.Measure.withDensity
Proof uses: MeasureTheory.Measure.IsOpenPosMeasure.mk, Set, IsOpen, Set.Nonempty, ne_of_gt, lt_of_lt_of_le, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, TopologicalSpace.PositiveCompacts, LE.le, Exists, LT.lt, exists_positiveCompacts_subset, And, Membership.mem, IsMinOn, IsCompact.exists_isMinOn, TopologicalSpace.PositiveCompacts.isCompact, TopologicalSpace.PositiveCompacts.nonempty, Continuous.continuousOn and 29 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Measure.haarScalarFactor_symm line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, IsTopologicalGroup, MeasurableSpace, BorelSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsHaarMeasure, Eq, NNReal, MeasureTheory.Measure.haarScalarFactor, Inv.inv
Proof uses: eq_inv_of_mul_eq_one_left, Eq.mpr, HMul.hMul, OfNat.ofNat, id, congrArg, Eq.symm, MeasureTheory.Measure.haarScalarFactor_eq_mul, MeasureTheory.Measure.haarScalarFactor_self, Eq.refl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.modularCharacter_eq_mulEquivHaarChar line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, IsTopologicalGroup, LocallyCompactSpace, MeasurableSpace, BorelSpace, Eq, NNReal, MonoidHom, MeasureTheory.Measure.modularCharacter, MeasureTheory.mulEquivHaarChar, MulDistribMulAction.toContinuousMulEquiv, ConjAct, MulEquiv, ConjAct.toConjAct
Proof uses: Eq.mpr, Inv.inv, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, inv_inv, map_inv, MeasureTheory.Measure.haarScalarFactor, MeasureTheory.Measure.haar, MeasureTheory.Measure.map, HMul.hMul, Classical.arbitrary, TopologicalSpace.PositiveCompacts, ContinuousMulEquiv, congrFun', MeasureTheory.Measure.IsHaarMeasure, MeasureTheory.Measure.modularCharacterFun_eq_haarScalarFactor and 9 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Measure.conjAct_smul line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, IsTopologicalGroup, LocallyCompactSpace, MeasurableSpace, BorelSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsHaarMeasure, MeasureTheory.Measure.Regular, ConjAct, Set, Eq, ENNReal, HSMul.hSMul, Set.smulSet, HMul.hMul, MonoidHom, NNReal, MeasureTheory.Measure.modularCharacter, MulEquiv and 1 more
Proof uses: Eq.mpr, MeasureTheory.mulEquivHaarChar, MulDistribMulAction.toContinuousMulEquiv, ConjAct.toConjAct, id, congrArg, MeasureTheory.modularCharacter_eq_mulEquivHaarChar, Eq.symm, smul_eq_mul, MeasureTheory.Measure.smul_apply, MeasureTheory.Measure.coe_nnreal_smul, MeasureTheory.Measure.comap, ContinuousMulEquiv, MeasureTheory.mulEquivHaarChar_smul_eq_comap, Set.preimage, MeasurableEquiv, MeasurableEquiv.symm, Homeomorph.toMeasurableEquiv, ContinuousMulEquiv.toHomeomorph, eq_of_heq and 13 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.relIndex_mul_measure line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Group, MeasurableMul, Subgroup, Subgroup.IsFiniteRelIndex, MeasurableSet, LE.le, MeasureTheory.Measure, MeasureTheory.Measure.IsMulLeftInvariant, Eq, ENNReal, HMul.hMul, Subgroup.relIndex, Set
Proof uses: Set.iUnion, HasQuotient.Quotient, Subtype, Membership.mem, Subgroup.subgroupOf, HSMul.hSMul, Set.smulSet, Quotient.out, QuotientGroup.leftRel, Eq.mpr, Set.image, Set.univ, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, of_eq_true, Eq.trans, True and 53 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
class IsUnimodularGroup A group with topolgoy is a unimodular group if it is a locally compact topological group such that the modular character is trivial line 130 source
Source documentation
A group with topolgoy is a unimodular group if it is a locally compact topological group such that the modular character is trivial. (i.e. left haar measure = right haar measure)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
class IsUnimodularGroup (G : Type*) [TopologicalSpace G] [Group G] : Prop extends
    IsTopologicalGroup G, LocallyCompactSpace G where
…
```
instance (instance at line 134) line 134 source
lemma modularCharacter_mul_relIndex_conjAct Documented declaration: modularCharacter_mul_relIndex_conjAct line 149 source
Source documentation
If G is a locally compact group, and K₁, K₂ are compact open subgroups of G such that K₁ contains both K₁ and gK₁g⁻¹, then Δ(g) * [K₂ : gK₁g⁻¹] = [K₂ : K₁], where Δ is the modular character.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, IsTopologicalGroup, LocallyCompactSpace, Subgroup, IsOpen, IsCompact, ConjAct, LE.le, HSMul.hSMul, Subgroup.pointwiseMulAction, Eq, NNReal, HMul.hMul, MonoidHom, MeasureTheory.Measure.modularCharacter, MulEquiv, ConjAct.ofConjAct, Subgroup.relIndex
Proof uses: Subgroup.IsFiniteRelIndex, Subgroup.IsFiniteRelIndex.of_isCompact, IsOpen.smul, MeasurableSpace, borel, BorelSpace, BorelSpace.mk, rfl, ENNReal.coe_injective, Iff.mp, ENNReal, MeasureTheory.Measure, Set, MeasureTheory.Measure.haar, ENNReal.mul_left_inj, IsOpen.measure_ne_zero, Classical.arbitrary, TopologicalSpace.PositiveCompacts, of_eq_true, Set.Nonempty and 34 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma modularCharacter_mul_relIndex_conjAct
    {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [LocallyCompactSpace G] {K₁ K₂ : Subgroup G}
    (hOpen : IsOpen (X := G) K₁) (hCompact : IsCompact (X := G) K₂)
…
```
lemma relIndex_conjAct_eq If G is a unimodular group, and K₁, K₂ are compact open subgroups of G such that K₁ contains both K₁ and gK₁g⁻¹, then [K₂ : gK₁g⁻¹] = [K₂ : K₁] line 173 source
Source documentation
If G is a unimodular group, and K₁, K₂ are compact open subgroups of G such that K₁ contains both K₁ and gK₁g⁻¹, then [K₂ : gK₁g⁻¹] = [K₂ : K₁].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, IsUnimodularGroup, Subgroup, IsOpen, IsCompact, ConjAct, LE.le, HSMul.hSMul, Subgroup.pointwiseMulAction, Eq, Nat, Subgroup.relIndex
Proof uses: Eq.mp, NNReal, HMul.hMul, MonoidHom, MeasureTheory.Measure.modularCharacter, MulEquiv, ConjAct.ofConjAct, Eq.trans, congrFun', congrArg, OfNat.ofNat, IsUnimodularGroup.modularCharacter_eq_one, one_mul, modularCharacter_mul_relIndex_conjAct
53 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma relIndex_conjAct_eq
    {G : Type*} [TopologicalSpace G] [Group G] [IsUnimodularGroup G] {K₁ K₂ : Subgroup G}
    (hOpen : IsOpen (X := G) K₁) (hCompact : IsCompact (X := G) K₂)
…
```
Mentions: IsUnimodularGroup
lemma relIndex_conjAct_inv_smul_self If G is a unimodular group, and K₁, K₂ are compact open subgroups of G such that K₁ contains both K₁ and gK₁g⁻¹, then [K₂ : gK₁g⁻¹] = [K₂ : K₁] line 185 source
Source documentation
If G is a unimodular group, and K₁, K₂ are compact open subgroups of G such that K₁ contains both K₁ and gK₁g⁻¹, then [K₂ : gK₁g⁻¹] = [K₂ : K₁].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, IsUnimodularGroup, Subgroup, IsOpen, IsCompact, ConjAct, Eq, Nat, Subgroup.relIndex, HSMul.hSMul, Subgroup.pointwiseMulAction, Inv.inv
Proof uses: Eq.mp, Min.min, congr, congrArg, Eq.trans, congrFun', Subgroup.smul_inf, inv_smul_smul, Subgroup.inf_relIndex_left, Subgroup.inf_relIndex_right, relIndex_conjAct_eq, IsOpen.inter, Set, Set.smulSet, Submonoid, Subgroup.toSubmonoid, IsOpen.smul, of_eq_true, LE.le, True
48 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma relIndex_conjAct_inv_smul_self
    {G : Type*} [TopologicalSpace G] [Group G] [IsUnimodularGroup G] {K : Subgroup G}
    (hOpen : IsOpen (X := G) K) (hCompact : IsCompact (X := G) K)
…
```
Mentions: IsUnimodularGroup
lemma exists_bijOn_mk_image_mul_singleton_and_mk_image_mul_singleton_inv There exists a set of coset representatives βᵢ of UgU such that UgU = ⨆ βᵢgU and Ug⁻¹U = ⨆ βᵢ⁻¹g⁻¹U line 197 source
Source documentation
There exists a set of coset representatives βᵢ of UgU such that UgU = ⨆ βᵢgU and Ug⁻¹U = ⨆ βᵢ⁻¹g⁻¹U

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, IsUnimodularGroup, Subgroup, IsOpen, IsCompact, Exists, Finset, And, Set.BijOn, HasQuotient.Quotient, Set.image, HMul.hMul, Set, Set.mul, Singleton.singleton, Function.comp, Inv.inv
Proof uses: Nat, Subgroup.relIndex, HSMul.hSMul, ConjAct, Subgroup.pointwiseMulAction, MulEquiv, ConjAct.toConjAct, Subgroup.IsFiniteRelIndex, Subgroup.IsFiniteRelIndex.of_isCompact, IsOpen.smul, Equiv, Fin, Equiv.trans, Nat.card, Subtype, Membership.mem, Subgroup.subgroupOf, Equiv.symm, Finite.equivFin, QuotientGroup.quotientConjActEquivImageMulSingleton and 63 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
lemma exists_bijOn_mk_image_mul_singleton_and_mk_image_mul_singleton_inv
    {G : Type*} [Group G] [TopologicalSpace G] [IsUnimodularGroup G]
    (U : Subgroup G) (hOpen : IsOpen (X := G) U) (hCompact : IsCompact (X := G) U) (g : G) :
…
```
Mentions: IsUnimodularGroup
instance MeasureTheory.Units.instMeasurableSpace line 234 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monoid, MeasurableSpace, Units
Proof uses: MeasurableSpace.comap, Prod, MulOpposite, MonoidHom, Units.embedProduct, inferInstance
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.(instance at line 237) line 237 source
lemma MeasureTheory.Units.measurableEmbedding_val line 243 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monoid, TopologicalSpace, ContinuousMul, MeasurableSpace, BorelSpace, PolishSpace, MeasurableEmbedding, Units
Proof uses: Continuous.measurableEmbedding, Units.continuous_val, Units.val_injective
17 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.Units.measurableEmbedding_val' line 248 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monoid, TopologicalSpace, MeasurableSpace, BorelSpace, SecondCountableTopology, IsOpenUnits, MeasurableEmbedding, Units
Proof uses: Topology.IsOpenEmbedding.measurableEmbedding, IsOpenUnits.isOpenEmbedding_unitsVal
6 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.isMulLeftInvariant_map_op line 256 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monoid, MeasurableSpace, MeasurableMul, MeasureTheory.Measure, Iff, MeasureTheory.Measure.IsMulLeftInvariant, MulOpposite, MeasureTheory.Measure.map, MulOpposite.op, MeasureTheory.Measure.IsMulRightInvariant
Proof uses: Eq.mpr, Eq, HMul.hMul, id, congrArg, propext, MeasureTheory.Measure.isMulLeftInvariant_iff, MeasureTheory.Measure.isMulRightInvariant_iff, MeasurableEquiv, MulOpposite.opMeasurableEquiv, forall_congr, Eq.symm, Function.Injective.eq_iff, MeasurableEmbedding.map_injective, MeasurableEquiv.measurableEmbedding, Function.comp, congr, Eq.trans, congrFun', MeasureTheory.Measure.map_map and 6 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.Units.haarMeasure Given a locally compact topological ring R such that Rˣ → R is an open embedding line 270 source
Source documentation
Given a locally compact topological ring R such that Rˣ → R is an open embedding. If dx is an additive haar measure on R, then dx/δ(x) is a multiplicative haar measure on Rˣ, where δ is the Haar character.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, MeasureTheory.Measure, BorelSpace, Units
Proof uses: MeasureTheory.Measure.withDensity, MeasureTheory.Measure.comap, ContinuousMonoidHom, NNReal, MeasureTheory.ringHaarChar, Inv.inv
19 instances, coercions and auxiliary constants left out.
```
noncomputable def Units.haarMeasure [BorelSpace R] : Measure Rˣ :=
…
```
lemma MeasureTheory.Units.haarMeasure_apply Can replace IsOpenUnits R + SecondCountableTopology R by PolishSpace R line 275 source
Source documentation
Can replace IsOpenUnits R + SecondCountableTopology R by PolishSpace R.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, MeasureTheory.Measure, BorelSpace, IsOpenUnits, SecondCountableTopology, Set, Units, MeasurableSet, Eq, ENNReal, MeasureTheory.Units.haarMeasure, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Set.image, dite, IsUnit and 9 more
Proof uses: id, Eq.mpr, MeasureTheory.Measure.withDensity, MeasureTheory.Measure.comap, congrArg, MeasureTheory.withDensity_apply, MeasureTheory.Measure.map, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, funext, of_eq_true, Eq.trans, True, congr, map_inv, dite_eq_left_of_eq_true, IsUnit.unit_of_val_units and 13 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
lemma Units.haarMeasure_apply [BorelSpace R] [IsOpenUnits R] [SecondCountableTopology R]
    (s : Set Rˣ) (hs : MeasurableSet s) :
    Units.haarMeasure μ s = ∫⁻ (a : R) in Units.val '' s,
      if h : IsUnit a then ↑(ringHaarChar h.unit⁻¹) else 0 ∂μ := by
…
```
Mentions: MeasureTheory.Units.haarMeasure, MeasureTheory.ringHaarChar
instance MeasureTheory.(instance at line 289) line 289 source
instance MeasureTheory.(instance at line 295) line 295 source
instance MeasureTheory.(instance at line 301) line 301 source
instance MeasureTheory.(instance at line 309) line 309 source
lemma MeasureTheory.Units.isMulRightInvariant_haarMeasure line 335 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, MeasureTheory.Measure, BorelSpace, MeasureTheory.Measure.IsAddHaarMeasure, IsOpenUnits, SecondCountableTopology, T1Space, Units, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, MulOpposite, MulEquiv, MulEquiv.symm, Units.opEquiv and 3 more
Proof uses: MeasureTheory.Measure.comap, MeasurableEquiv, MeasurableEquiv.symm, Homeomorph.toMeasurableEquiv, MulOpposite.opHomeomorph, MeasureTheory.Measure.IsAddHaarMeasure.comap, inferInstance, MeasurableAdd, AddEquiv.toAddMonoidHom, AddEquiv.symm, MulOpposite.opAddEquiv, Homeomorph.isOpenEmbedding, Homeomorph.symm, MeasureTheory.Measure.IsMulLeftInvariant, MonoidHom, MulEquiv.toMonoidHom, ContinuousMulEquiv.toMulEquiv, ContinuousMulEquiv.symm, Units.opContinuousMulEquiv, MeasureTheory.Measure.IsMulLeftInvariant.comap and 69 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Units.isUnimodularGroup line 364 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, T1Space, SecondCountableTopology, IsOpenUnits, Units, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, MulOpposite, MulEquiv, MulEquiv.symm, Units.opEquiv, MulOpposite.op, IsUnimodularGroup
Proof uses: IsUnimodularGroup.mk, MonoidHom.ext, MeasureTheory.Measure.modularCharacter, OfNat.ofNat, MonoidHom, Eq.trans, MeasureTheory.Measure.modularCharacterFun, MeasureTheory.Measure.haarScalarFactor, MeasureTheory.Measure.map, HMul.hMul, MeasureTheory.Units.haarMeasure, MeasureTheory.Measure.addHaar, Classical.arbitrary, TopologicalSpace.PositiveCompacts, MeasureTheory.Measure.modularCharacterFun_eq_haarScalarFactor, MeasureTheory.Measure.IsMulRightInvariant, MeasureTheory.Units.isMulRightInvariant_haarMeasure, Eq.mpr, Eq.rec, MeasureTheory.Measure and 7 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.Matrix.instMeasurableSpace line 380 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Matrix
1 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.(instance at line 383) line 383 source
instance MeasureTheory.(instance at line 386) line 386 source
instance MeasureTheory.(instance at line 389) line 389 source
instance MeasureTheory.(instance at line 392) line 392 source
instance MeasureTheory.(instance at line 395) line 395 source
instance MeasureTheory.(instance at line 401) line 401 source
instance MeasureTheory.(instance at line 404) line 404 source
lemma MeasureTheory.Matrix.ringHaarChar_eq_of_field line 424 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, IsTopologicalDivisionRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, SecondCountableTopology, Fintype, DecidableEq, Units, Matrix, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, HPow.hPow, Nat, MonoidHom, Units.map, Matrix.detMonoidHom and 1 more
Proof uses: Eq.trans, MeasureTheory.addEquivAddHaarChar, ContinuousLinearEquiv.toContinuousAddEquiv, ContinuousAddEquiv, ContinuousAddEquiv.mulLeft, ContinuousLinearEquiv.mk, RingHom.id, LinearEquiv.mk, LinearMap.mk, AddHom.mk, Equiv.toFun, AddEquiv.toEquiv, ContinuousAddEquiv.toAddEquiv, AddEquiv.map_add', of_eq_true, HSMul.hSMul, RingHom, HMul.hMul, True, congr and 28 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Measure.haarScalarFactor_map' line 436 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, MeasurableSpace, BorelSpace, IsTopologicalGroup, MeasureTheory.Measure, MeasureTheory.Measure.IsHaarMeasure, ContinuousMulEquiv, Eq, NNReal, MeasureTheory.Measure.haarScalarFactor, MeasureTheory.Measure.map
Proof uses: dite, LocallyCompactSpace, Classical.propDecidable, Topology.IsOpenEmbedding.locallyCompactSpace, Homeomorph, ContinuousMulEquiv.toHomeomorph, ContinuousMulEquiv.symm, Homeomorph.isOpenEmbedding, ContinuousMap, Real, And, HasCompactSupport, LE.le, OfNat.ofNat, Ne, Exists, exists_continuous_nonneg_pos, Continuous, ContinuousMap.mk, MeasureTheory.integral and 36 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.mulEquivHaarChar_conj line 462 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, MeasurableSpace, BorelSpace, IsTopologicalGroup, LocallyCompactSpace, ContinuousMulEquiv, Eq, NNReal, MeasureTheory.mulEquivHaarChar, ContinuousMulEquiv.trans, ContinuousMulEquiv.symm
Proof uses: MeasureTheory.Measure.IsHaarMeasure, MeasureTheory.Measure.comap, MeasureTheory.Measure.haar, MeasureTheory.Measure.IsHaarMeasure.comap, inferInstance, MeasurableMul, Classical.arbitrary, TopologicalSpace.PositiveCompacts, MulEquiv.toMonoidHom, ContinuousMulEquiv.toMulEquiv, Homeomorph.isOpenEmbedding, ContinuousMulEquiv.toHomeomorph, MeasureTheory.Measure.Regular, MeasureTheory.Measure.Regular.comap, MeasureTheory.Measure, MeasureTheory.Measure.map, MeasurableEquiv.map_symm, Homeomorph.toMeasurableEquiv, Eq.mpr, MeasureTheory.Measure.haarScalarFactor and 21 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.mulEquivHaarChar_conj' line 479 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, MeasurableSpace, BorelSpace, IsTopologicalGroup, LocallyCompactSpace, ContinuousMulEquiv, Eq, NNReal, MeasureTheory.mulEquivHaarChar, ContinuousMulEquiv.trans, ContinuousMulEquiv.symm
Proof uses: MeasureTheory.mulEquivHaarChar_conj
10 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.Measure.modularCharacter_comp line 488 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, IsTopologicalGroup, LocallyCompactSpace, ContinuousMulEquiv, Eq, NNReal, MonoidHom, MeasureTheory.Measure.modularCharacter
Proof uses: Eq.mpr, MeasureTheory.mulEquivHaarChar, borel, BorelSpace.mk, rfl, MeasurableSpace, MulDistribMulAction.toContinuousMulEquiv, ConjAct, MulEquiv, ConjAct.toConjAct, id, congrArg, MeasureTheory.modularCharacter_eq_mulEquivHaarChar, ContinuousMulEquiv.trans, ContinuousMulEquiv.symm, Eq.symm, MeasureTheory.mulEquivHaarChar_conj, BorelSpace, Eq.rec, Eq.refl and 12 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.ContinuousMulEquiv.isUnimodularGroup line 498 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, IsUnimodularGroup, ContinuousMulEquiv
Proof uses: IsTopologicalGroup, ContinuousMulEquiv.isTopologicalGroup, LocallyCompactSpace, Topology.IsOpenEmbedding.locallyCompactSpace, Homeomorph, ContinuousMulEquiv.toHomeomorph, Homeomorph.isOpenEmbedding, IsUnimodularGroup.mk, MonoidHom.ext, NNReal, MeasureTheory.Measure.modularCharacter, OfNat.ofNat, MonoidHom, NNReal.eq, Eq.mpr, Eq, Real, id, congrArg, Eq.symm and 7 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.ringHaarChar_of_isHomeomorph line 508 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, RingHom, IsHomeomorph, Units, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, MonoidHom, Units.map
Proof uses: ContinuousAddEquiv, Homeomorph, IsHomeomorph.homeomorph, ContinuousAddEquiv.mk, AddEquiv.mk, Homeomorph.toEquiv, RingHom.map_add', Homeomorph.continuous_toFun, Homeomorph.continuous_invFun, ContinuousAddEquiv.symm, ContinuousAddEquiv.symm_apply_apply, Eq.mpr, MeasureTheory.addEquivAddHaarChar, ContinuousAddEquiv.mulLeft, id, congrArg, MeasureTheory.ringHaarChar_apply, ContinuousAddEquiv.trans, Eq.symm, MeasureTheory.addEquivAddHaarChar_conj and 11 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.Matrix.mopContinuousMulEquiv For any ring R, we have ring isomorphism Matₙₓₙ(Rᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ given by transpose line 529 source
Source documentation
For any ring R, we have ring isomorphism Matₙₓₙ(Rᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ given by transpose.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Mul, AddCommMonoid, TopologicalSpace, ContinuousMulEquiv, Matrix, MulOpposite
Proof uses: RingEquiv, RingEquiv.mopMatrix, ContinuousMulEquiv.mk, MulEquiv.mk, RingEquiv.toEquiv
18 instances, coercions and auxiliary constants left out.
```
def Matrix.mopContinuousMulEquiv {m α} [Fintype m] [Mul α] [AddCommMonoid α]
    [TopologicalSpace α] :
    Matrix m m αᵐᵒᵖ ≃ₜ* (Matrix m m α)ᵐᵒᵖ where
…
```
def MeasureTheory.Matrix.transposeContinuousMulEquiv For any ring R, we have ring isomorphism Matₙₓₙ(Rᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ given by transpose line 539 source
Source documentation
For any ring R, we have ring isomorphism Matₙₓₙ(Rᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ given by transpose.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, CommMagma, AddCommMonoid, TopologicalSpace, ContinuousMulEquiv, Matrix, MulOpposite
Proof uses: RingEquiv, Matrix.transposeRingEquiv, ContinuousMulEquiv.mk, MulEquiv.mk, RingEquiv.toEquiv
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def Matrix.transposeContinuousMulEquiv {m α} [Fintype m]
    [CommMagma α] [AddCommMonoid α] [TopologicalSpace α] :
    Matrix m m α ≃ₜ* (Matrix m m α)ᵐᵒᵖ where
…
```
lemma MeasureTheory.Matrix.ringHaarChar_eq_ringHaarChar_opEquiv line 546 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, IsTopologicalDivisionRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, SecondCountableTopology, Fintype, DecidableEq, Units, Matrix, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, MulOpposite, MulEquiv, MulEquiv.symm, Units.opEquiv, MulOpposite.op
Proof uses: Eq.mpr, HPow.hPow, Nat, MonoidHom, Units.map, Matrix.detMonoidHom, Fintype.card, id, congrArg, MeasureTheory.Matrix.ringHaarChar_eq_of_field, RingEquiv.toRingHom, RingEquiv.symm, Matrix.transposeRingEquiv, Eq.symm, MeasureTheory.ringHaarChar_of_isHomeomorph, Homeomorph.isHomeomorph, ContinuousMulEquiv.toHomeomorph, ContinuousMulEquiv.symm, MeasureTheory.Matrix.transposeContinuousMulEquiv, HPow and 18 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.(instance at line 557) line 557 source