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 95 research declarations. Search 10,000 more complete Mathlib declarations.
95 results
Clear filtersMaximalPQuotient.isPGroup_of_isTorsion
Plain-language statement
The "maximal p-quotient" of (ℤ, +) is ℤ/⋂ₙ pⁿℤ = ℤ, not a p-group.
Source project: Fermat's Last Theorem
Person-level attribution pending.
MeasureTheory.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.