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 91 research declarations. Search 10,000 more complete Mathlib declarations.
91 results
Clear filtersMeasureTheory.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.
NumberField.AdeleRing.addEquivAddHaarChar_mulRight_unit_eq_one
Plain-language statement
Right multiplication by an element of Bˣ on B ⊗ 𝔸_K does not scale additive Haar measure.
Source project: Fermat's Last Theorem
Person-level attribution pending.
NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_real_surjective
Plain-language statement
For any positive real r, there's some ρ ∈ ℝˣ such that the haar character of (ρ, 1) ∈ D_f × D_∞ is r.
Source project: Fermat's Last Theorem
Person-level attribution pending.
NumberField.AdeleRing.units_mem_ringHaarCharacter_ker
Plain-language statement
Left multiplication by an element of Bˣ on B ⊗ 𝔸_K does not scale additive Haar measure. In other words, Bˣ is in the kernel of the ringHaarChar of B ⊗ 𝔸_K.
Source project: Fermat's Last Theorem
Person-level attribution pending.