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

10 declarations, 0 contain sorry, 0 declared as axioms

Haar character scaling under linear automorphisms

We prove that a linear isomorphism on a finite-dimensional vector space V over a locally compact field F scales Haar measure by its determinant. The proof assumes [SecondCountableTopology F].

We proceed by:

Proving the scaling property for diagonal matrices.
Showing that transvections preserve Haar measure.
Extending to arbitrary matrices using induction on diagonal/transvection decomposition.
Proving the result for automorphisms on (ι → F)
Deducing the general result for V

Main result

addEquivAddHaarChar_eq_ringHaarChar_det

TODO

Review [SecondCountableTopology F] assumption
Consider generalisation to commutative rings

Imports (9)

Imported by 4 files

lemma MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_diagonal A diagonal matrix scales addHaar with its determinant line 64 source
Source documentation
A diagonal matrix scales addHaar with its determinant

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, MeasurableSpace, TopologicalSpace, BorelSpace, LocallyCompactSpace, CommRing, IsTopologicalRing, SecondCountableTopology, ContinuousLinearEquiv, RingHom.id, Eq, Matrix, LinearEquiv, LinearMap, LinearMap.toMatrix', Matrix.diagonal, NNReal, MeasureTheory.addEquivAddHaarChar, ContinuousLinearEquiv.toContinuousAddEquiv and 5 more
Proof uses: Matrix.toLin', Eq.mpr, id, congrArg, Eq.symm, Matrix.toLin'_toMatrix', Eq.refl, LinearMap.det, Finset.prod, Finset.univ, Matrix.det, LinearMap.det_toLin', Matrix.det_diagonal, IsUnit, Iff.mp, IsUnit.prod_univ_iff, LinearEquiv.isUnit_det', ContinuousAddEquiv, ContinuousAddEquiv.piCongrRight, ContinuousAddEquiv.mulLeft and 10 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma addEquivAddHaarChar_eq_ringHaarChar_det_diagonal [SecondCountableTopology F]
    (ρ : (ι → F) ≃L[F] (ι → F)) {D : ι → F}
    (h : ρ.toLinearMap.toMatrix' = Matrix.diagonal D) :
    addEquivAddHaarChar ρ.toContinuousAddEquiv = ringHaarChar ρ.toLinearEquiv.det := by
…
```
Mentions: MeasureTheory.ringHaarChar
lemma MeasureTheory.Matrix.TransvectionStruct.measurePreserving A transvection preserves addHaar on ι → F line 89 source
Source documentation
A transvection preserves addHaar on ι → F.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, MeasurableSpace, TopologicalSpace, BorelSpace, LocallyCompactSpace, CommRing, IsTopologicalRing, SecondCountableTopology, Matrix.TransvectionStruct, MeasureTheory.MeasurePreserving, LinearMap, RingHom.id, LinearEquiv, Matrix, Matrix.toLin', Matrix.TransvectionStruct.toMatrix, MeasureTheory.Measure.addHaar
Proof uses: MeasureTheory.Measure, MeasureTheory.Measure.pi, Continuous, LinearMap.continuous_on_pi, Measurable, Continuous.measurable, MeasureTheory.MeasurePreserving.mk, Eq.symm, MeasureTheory.Measure.map, MeasureTheory.Measure.pi_eq, Classical.arbitrary, TopologicalSpace.PositiveCompacts, Set, MeasurableSet, Set.pi, Set.univ, MeasurableSet.univ_pi, Eq.mpr, Eq, ENNReal and 51 more
171 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma Matrix.TransvectionStruct.measurePreserving [SecondCountableTopology F]
    (t : Matrix.TransvectionStruct ι F) :
    MeasurePreserving (⇑(Matrix.toLin' t.toMatrix)) addHaar addHaar := by
…
```
lemma MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_matrix_pi Haar measure scaling on (ι → F) for continuous linear equivalences generated by a matrix line 125 source
Source documentation
Haar measure scaling on (ι → F) for continuous linear equivalences generated by a matrix

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, MeasurableSpace, TopologicalSpace, BorelSpace, LocallyCompactSpace, CommRing, IsTopologicalRing, SecondCountableTopology, Matrix, Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec, IsUnit, Matrix.det, Module.Basis, Pi.basisFun, ContinuousLinearEquiv, RingHom.id, Matrix.toContinuousLinearEquiv, Eq, NNReal and 8 more
Proof uses: Matrix.diagonal_transvection_induction_of_det_unit, Matrix.diagonal, Eq.mpr, id, congrArg, rfl, LinearMap, LinearMap.toMatrix', Matrix.toContinousLinearEquiv_toMatrix, MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_diagonal, Eq.refl, Matrix.TransvectionStruct, Matrix.TransvectionStruct.toMatrix, OfNat.ofNat, ContinuousAddEquiv, Matrix.toLin', of_eq_true, Eq.trans, True, congrFun' and 34 more
164 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma addEquivAddHaarChar_eq_ringHaarChar_det_matrix_pi [SecondCountableTopology F]
    (M : Matrix ι ι F) (hM : Pivot.ExistsListTransvecMulDiagonalMulListTransvec M)
    (h : IsUnit M.det) :
    let b := Pi.basisFun F ι
…
```
lemma MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_pi Haar measure scaling for linear maps on (ι → F) line 177 source
Source documentation
Haar measure scaling for linear maps on (ι → F)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, MeasurableSpace, TopologicalSpace, BorelSpace, LocallyCompactSpace, CommRing, IsTopologicalRing, SecondCountableTopology, ContinuousLinearEquiv, RingHom.id, Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec, LinearEquiv, LinearMap, Matrix, LinearMap.toMatrix, Pi.basisFun, Eq, NNReal, MeasureTheory.addEquivAddHaarChar and 6 more
Proof uses: Module.Basis, IsUnit, Matrix.det, of_eq_true, Eq.trans, LinearMap.det, True, congrArg, LinearMap.det_toMatrix, Matrix.toContinuousLinearEquiv, Eq.symm, ContinuousLinearEquiv.toMatrix_isUnit_det, ContinuousLinearEquiv.toMatrix_toContinousLinearEquiv, Eq.mpr, id, MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_matrix_pi
128 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma addEquivAddHaarChar_eq_ringHaarChar_det_pi [SecondCountableTopology F]
    (ρ : (ι → F) ≃L[F] (ι → F))
    (hρM : Pivot.ExistsListTransvecMulDiagonalMulListTransvec
      (ρ.toLinearEquiv.toMatrix (Pi.basisFun F ι) (Pi.basisFun F ι))) :
    addEquivAddHaarChar ρ.toContinuousAddEquiv = ringHaarChar ρ.toLinearEquiv.det := by
…
```
Mentions: MeasureTheory.ringHaarChar
theorem MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc Haar measure scaling for invertible linear maps on a finite-dimensional vector space over a field F assuming [SecondCountableTopology F] line 204 source
Source documentation
Haar measure scaling for invertible linear maps on a finite-dimensional vector space over a field F assuming [SecondCountableTopology F].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, BorelSpace, LocallyCompactSpace, CommRing, IsTopologicalRing, AddCommGroup, Module, IsModuleTopology, IsTopologicalAddGroup, SecondCountableTopology, ContinuousLinearEquiv, RingHom.id, Nat, Module.Basis, Fin, Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec, LinearEquiv, LinearMap, Matrix and 10 more
Proof uses: Module.Basis.equivFun, Continuous, IsModuleTopology.continuous_of_linearMap, LinearEquiv.symm, ContinuousLinearEquiv.mk, ContinuousAddEquiv, ContinuousAddEquiv.trans, ContinuousAddEquiv.symm, of_eq_true, Eq.trans, True, forall_congr, eq_self, implies_true, MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv, ContinuousLinearEquiv.trans, ContinuousLinearEquiv.symm, rfl, MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_pi, congrFun' and 7 more
152 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc
    [SecondCountableTopology F] (ρ : V ≃L[F] V) (n : ℕ) (b : Basis (Fin n) F V)
    (hρ : Pivot.ExistsListTransvecMulDiagonalMulListTransvec
      (ρ.toLinearMap.toMatrix b b)) :
    addEquivAddHaarChar ρ.toContinuousAddEquiv = ringHaarChar ρ.toLinearEquiv.det := by
…
```
Mentions: MeasureTheory.ringHaarChar
theorem MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det Haar measure scaling for invertible linear maps on a finite-dimensional vector space over a field F assuming [SecondCountableTopology F] line 244 source
Source documentation
Haar measure scaling for invertible linear maps on a finite-dimensional vector space over a field F assuming [SecondCountableTopology F].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, BorelSpace, LocallyCompactSpace, Field, IsTopologicalRing, AddCommGroup, Module, FiniteDimensional, IsModuleTopology, IsTopologicalAddGroup, SecondCountableTopology, ContinuousLinearEquiv, RingHom.id, Eq, NNReal, MeasureTheory.addEquivAddHaarChar, ContinuousLinearEquiv.toContinuousAddEquiv, ContinuousMonoidHom, Units and 4 more
Proof uses: MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc, Module.finrank, Module.finBasis, Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec', Fin, LinearMap, Matrix, LinearMap.toMatrix
103 instances, coercions and auxiliary constants left out.
```
theorem addEquivAddHaarChar_eq_ringHaarChar_det [SecondCountableTopology F] (ρ : V ≃L[F] V) :
    addEquivAddHaarChar ρ.toContinuousAddEquiv = ringHaarChar ρ.toLinearEquiv.det :=
…
```
Mentions: MeasureTheory.ringHaarChar
def MeasureTheory._root_.ContinuousLinearEquiv.mulLeft Multiplication on the left by a unit of an F-algebra which is a topological ring, is a continuous F-linear homeomorphism line 270 source
Source documentation
Multiplication on the left by a unit of an F-algebra which is a topological ring, is a continuous F-linear homeomorphism.
```
def _root_.ContinuousLinearEquiv.mulLeft (u : Aˣ) : A ≃L[R] A where
…
```
def MeasureTheory._root_.ContinuousLinearEquiv.mulRight Multiplication on the right by a unit of an F-algebra which is a topological ring, is a continuous F-linear homeomorphism line 280 source
Source documentation
Multiplication on the right by a unit of an F-algebra which is a topological ring, is a continuous F-linear homeomorphism.
```
def _root_.ContinuousLinearEquiv.mulRight (u : Aˣ) : A ≃L[R] A where
…
```
lemma MeasureTheory.algebra_ringHaarChar_eq_ringHaarChar_det line 297 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, MeasurableSpace, TopologicalSpace, BorelSpace, IsTopologicalRing, LocallyCompactSpace, Ring, Algebra, FiniteDimensional, IsModuleTopology, SecondCountableTopology, Units, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, MonoidHom, LinearEquiv, RingHom.id, LinearEquiv.det and 1 more
Proof uses: MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det, ContinuousLinearEquiv.mulLeft
53 instances, coercions and auxiliary constants left out.
lemma MeasureTheory._root_.IsSimpleRing.ringHaarChar_eq_addEquivAddHaarChar_mulRight line 317 source