Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 121 research declarations. Search 10,000 more complete Mathlib declarations.
121 results
Clear filtersMeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_diagonal
Plain-language statement
A diagonal matrix scales addHaar with its determinant
Source project: Fermat's Last Theorem
Person-level attribution pending.
MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc
Plain-language statement
Haar measure scaling for invertible linear maps on a finite-dimensional vector space over a field F assuming [SecondCountableTopology F].
Source project: Fermat's Last Theorem
Person-level attribution pending.
MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_pi
Plain-language statement
Haar measure scaling for linear maps on (ι → F)
Source project: Fermat's Last Theorem
Person-level attribution pending.
MeasureTheory.Matrix.TransvectionStruct.measurePreserving
Plain-language statement
A transvection preserves addHaar on ι → F.
Source project: Fermat's Last Theorem
Person-level attribution pending.
MeasureTheory.ringHaarChar_complex
Plain-language statement
The distributive Haar character of the action of ℂˣ on ℂ is the usual norm squared. This means that volume (z • s) = ‖z‖ ^ 2 * volume s for all z : ℂ and s : Set ℂ. See Complex.volume_complex_smul.
Source project: Fermat's Last Theorem
Person-level attribution pending.
MeasureTheory.ringHaarChar_padic
Plain-language statement
The distributive Haar character of the action of ℚ_[p]ˣ on ℚ_[p] is the usual p-adic norm. This means that volume (x • s) = ‖x‖ * volume s for all x : ℚ_[p] and s : Set ℚ_[p]. See Padic.volume_padic_smul
Source project: Fermat's Last Theorem
Person-level attribution pending.