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

17 declarations, 0 contain sorry, 0 declared as axioms

The ring Haar character

For a topological ring R, the unit Haar character ringHaarChar : Rˣ →ₜ* ℝ≥0 sending a unit u to the scaling factor of left multiplication by u on a fixed Haar measure on the additive group of R.

Imports (8)

Imported by 6 files

lemma ContinuousAddEquiv.preimage_mulLeft_smul line 35 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, Units, Set, Eq, Set.preimage, ContinuousAddEquiv, ContinuousAddEquiv.mulLeft, HSMul.hSMul, Set.smulSet
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, True, congrFun', congrArg, Exists, And, HMul.hMul, ContinuousAddEquiv.mulLeft_apply, funext, iff_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.ringHaarChar_continuous line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, Continuous, Units, NNReal, MeasureTheory.addEquivAddHaarChar, ContinuousAddEquiv.mulLeft
Proof uses: Real, ContinuousMap, And, HasCompactSupport, LE.le, OfNat.ofNat, Ne, Exists, exists_continuous_nonneg_pos, ContinuousMap.mk, MeasureTheory.integral, MeasureTheory.Measure.addHaar, ne_of_gt, Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero, Classical.arbitrary, TopologicalSpace.PositiveCompacts, Eq, HSMul.hSMul, MeasureTheory.Measure.map, ContinuousAddEquiv and 71 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.ringHaarChar Documented declaration: ringHaarChar line 85 source
Source documentation
ringHaarChar : Rˣ →ₜ* ℝ≥0 is the function sending a unit of a locally compact topological ring R to the positive real factor which left multiplication by the unit scales additive Haar measure by.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, ContinuousMonoidHom, Units, NNReal
Proof uses: ContinuousMonoidHom.mk, MonoidHom.mk, OneHom.mk, MeasureTheory.addEquivAddHaarChar, ContinuousAddEquiv.mulLeft, MeasureTheory.ringHaarChar_continuous
25 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
noncomputable def ringHaarChar : Rˣ →ₜ* ℝ≥0 where
…
```
lemma MeasureTheory.ringHaarChar_apply line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, Units, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, MeasureTheory.addEquivAddHaarChar, ContinuousAddEquiv.mulLeft
Proof uses: rfl
25 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.ringHaarChar_eq_ringHaarChar_of_continuousAlgEquiv Transport ringHaarChar across a continuous ℤ-algebra equivalence (in place of continuous ring equivalences since we don't have them) line 98 source
Source documentation
Transport ringHaarChar across a continuous ℤ-algebra equivalence (in place of continuous ring equivalences since we don't have them).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, ContinuousAlgEquiv, Int, Units, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, MonoidHom, Units.map, MulEquiv.toMonoidHom, AlgEquiv.toMulEquiv, ContinuousAlgEquiv.toAlgEquiv
Proof uses: MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv, ContinuousAddEquiv.mk, AddEquiv.mk, AlgEquiv.toEquiv, AlgEquiv.map_add', ContinuousAlgEquiv.continuous_toFun, ContinuousAlgEquiv.continuous_invFun, ContinuousAddEquiv.mulLeft, of_eq_true, ContinuousAddEquiv, Eq.trans, True, forall_congr, HMul.hMul, congr, congrArg, AlgEquiv, Equiv, Equiv.toFun, HAdd.hAdd and 12 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma ringHaarChar_eq_ringHaarChar_of_continuousAlgEquiv {S : Type*} [Ring S] [TopologicalSpace S]
    [IsTopologicalRing S] [LocallyCompactSpace S] [MeasurableSpace S] [BorelSpace S]
    (f : R ≃A[ℤ] S) (r : Rˣ) :
    ringHaarChar r = ringHaarChar (Units.map f.toMonoidHom r) :=
…
```
Mentions: MeasureTheory.ringHaarChar
lemma MeasureTheory.ringHaarChar_mul_integral line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsAddHaarMeasure, MeasureTheory.Measure.Regular, Real, Measurable, Units, Eq, HMul.hMul, ContinuousMonoidHom, NNReal, MeasureTheory.ringHaarChar, MeasureTheory.integral
Proof uses: Eq.symm, Eq.mpr, HSMul.hSMul, MeasureTheory.addEquivAddHaarChar, ContinuousAddEquiv.mulLeft, MeasureTheory.Measure.map, ContinuousAddEquiv, eq_of_heq, HEq, Eq.refl, HEq.refl, Or, OfNat.ofNat, id, Eq.trans, congrFun', congrArg, MeasureTheory.ringHaarChar_toFun, MeasureTheory.integral_map, Continuous.aemeasurable and 9 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.ringHaarChar_mul_volume line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsAddHaarMeasure, MeasureTheory.Measure.Regular, Set, Units, Eq, ENNReal, HSMul.hSMul, Set.smulSet, HMul.hMul, ContinuousMonoidHom, NNReal, MeasureTheory.ringHaarChar
Proof uses: Eq.mpr, MeasureTheory.addEquivAddHaarChar, ContinuousAddEquiv.mulLeft, id, congrArg, MeasureTheory.ringHaarChar_toFun, Set.preimage, ContinuousAddEquiv, Eq.symm, MeasureTheory.addEquivAddHaarChar_smul_preimage, of_eq_true, Eq.trans, True, congrFun', ContinuousAddEquiv.preimage_mulLeft_smul, eq_self
58 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.ringHaarChar_eq_of_measure_smul_eq_mul line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsAddHaarMeasure, MeasureTheory.Measure.Regular, Set, Ne, ENNReal, OfNat.ofNat, Top.top, NNReal, Units, Eq, HSMul.hSMul, Set.smulSet, HMul.hMul and 2 more
Proof uses: Eq.mp, congrArg, propext, ENNReal.mul_left_inj, MeasureTheory.ringHaarChar_mul_volume
51 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.ringHaarCharKer The kernel of the ringHaarChar : Rˣ → ℝ≥0, namely the units of a locally compact topological ring such that left multiplication by them does not change additive Haar measure line 137 source
Source documentation
The kernel of the ringHaarChar : Rˣ → ℝ≥0, namely the units of a locally compact topological ring such that left multiplication by them does not change additive Haar measure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, Subgroup, Units
Proof uses: MonoidHom.ker, NNReal, ContinuousMonoidHom.toMonoidHom, MeasureTheory.ringHaarChar
16 instances, coercions and auxiliary constants left out.
```
noncomputable def ringHaarCharKer := MonoidHom.ker (ringHaarChar : Rˣ →ₜ* ℝ≥0).toMonoidHom
```
Mentions: MeasureTheory.ringHaarChar
lemma MeasureTheory.mem_ringHaarChar_ker line 139 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, Units, Iff, Membership.mem, Subgroup, MeasureTheory.ringHaarCharKer, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, OfNat.ofNat
Proof uses: MonoidHom.mem_ker, ContinuousMonoidHom.toMonoidHom
26 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.ringHaarChar_prod Documented declaration: ringHaarChar_prod line 150 source
Source comment
this is true in general, but the proof is easier if we assume `SecondCountableTopologyEither R S` because then if R and S are equipped with the Borel sigma algebra, the product sigma algebra on R × S is also the Borel sigma algebra.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, Units, SecondCountableTopologyEither, Eq, NNReal, ContinuousMonoidHom, Prod, MeasureTheory.ringHaarChar, MulEquiv, MulEquiv.symm, MulEquiv.prodUnits, Prod.mk, HMul.hMul
Proof uses: MeasureTheory.addEquivAddHaarChar_prodCongr, ContinuousAddEquiv.mulLeft
33 instances, coercions and auxiliary constants left out.
```
lemma ringHaarChar_prod (u : Rˣ) (v : Sˣ) [SecondCountableTopologyEither R S] :
    ringHaarChar (MulEquiv.prodUnits.symm (u, v)) = ringHaarChar u * ringHaarChar v :=
…
```
Mentions: MeasureTheory.ringHaarChar
lemma MeasureTheory.ringHaarChar_prod' line 154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, Units, Prod, SecondCountableTopologyEither, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, HMul.hMul, Prod.fst, MulEquiv, MulEquiv.prodUnits, Prod.snd
Proof uses: MeasureTheory.ringHaarChar_prod
34 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.ringHaarChar_pi line 167 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, Fintype, SecondCountableTopology, Units, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, MulEquiv, MulEquiv.symm, MulEquiv.piUnits, Finset.prod, Finset.univ
Proof uses: MeasureTheory.addEquivAddHaarChar_piCongrRight, ContinuousAddEquiv.mulLeft
34 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.ringHaarChar_pi' line 171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, Fintype, SecondCountableTopology, Units, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, Finset.prod, Finset.univ, MulEquiv, MulEquiv.piUnits
Proof uses: MeasureTheory.addEquivAddHaarChar_piCongrRight, ContinuousAddEquiv.mulLeft
40 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.ringHaarChar_restrictedProduct line 190 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TopologicalSpace, IsTopologicalRing, LocallyCompactSpace, MeasurableSpace, BorelSpace, Subring, Fact, IsOpen, CompactSpace, Subtype, Membership.mem, SecondCountableTopology, Countable, Units, RestrictedProduct, Filter.cofinite, Eq, NNReal, ContinuousMonoidHom and 7 more
Proof uses: Eq.mpr, id, congrArg, rfl, MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight, Subring.toAddSubgroup, ContinuousAddEquiv.mulLeft, Filter.Eventually.mono, And, Set, Filter.sets, Set.ofPred, Inv.inv, Set.BijOn, ContinuousAddEquiv, AddSubgroup, Filter.Eventually.and, Subtype.coe_prop, And.intro, Set.MapsTo and 20 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.ringHaarChar_ModuleFinite line 210 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Ring, Algebra, Module.Finite, TopologicalSpace, IsTopologicalRing, IsModuleTopology, LocallyCompactSpace, MeasurableSpace, BorelSpace, SecondCountableTopology, Units, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, MonoidHom, Units.map, Algebra.algebraMap, Fin and 1 more
Proof uses: MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv, ContinuousLinearEquiv.toContinuousAddEquiv, IsModuleTopology.Module.Basis.equivFunHomeo, ContinuousAddEquiv.mulLeft, id, ContinuousAddEquiv, of_eq_true, ContinuousLinearEquiv, RingHom.id, RingHom, Eq.trans, HSMul.hSMul, True, congr, congrArg, HMul.hMul, ContinuousAddEquiv.mulLeft_apply, map_smul, eq_self
121 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.ringHaarChar_ModuleFinite_unit line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Ring, Algebra, Module.Finite, TopologicalSpace, IsTopologicalRing, IsModuleTopology, LocallyCompactSpace, MeasurableSpace, BorelSpace, SecondCountableTopology, Units, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, MonoidHom, Units.map, Algebra.algebraMap, HPow.hPow and 2 more
Proof uses: Eq.mpr, Fin, id, congrArg, MeasureTheory.ringHaarChar_ModuleFinite, Eq.mp, MulEquiv, MulEquiv.symm, MulEquiv.piUnits, Finset.prod, Finset.univ, Eq.trans, Finset.card, Finset.prod_const, Fintype.card_fin, MeasureTheory.ringHaarChar_pi
86 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.