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 5 research declarations. Search 10,000 more complete Mathlib declarations.
5 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.
TotallyDefiniteQuaternionAlgebra.finite_doubleCoset
Plain-language statement
For any open U ⊆ GL₂(𝔸_F), Dˣ\GL₂(𝔸_F)/U is finite. (where Dˣ is viewed as a subgroup of GL₂(𝔸_F) under the identification M₂(𝔸_F) ≃ D ⊗ 𝔸_F)
Source project: Fermat's Last Theorem
Person-level attribution pending.