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 filtersNumberField.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.
NumberField.FiniteAdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul
Plain-language statement
left multiplication and right multiplication by a unit have the same Haar character on B ⊗ 𝔸_K^f. See also NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul which proves it for 𝔸_K^f ⊗ B.
Source project: Fermat's Last Theorem
Person-level attribution pending.
NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul
Plain-language statement
left multiplication and right multiplication by a unit have the same Haar character on 𝔸_K^f ⊗ B. See also NumberField.FiniteAdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul which proves it for B ⊗ 𝔸_K^f.
Source project: Fermat's Last Theorem
Person-level attribution pending.
Padic.mulValuation_lt_iff_norm_lt
Plain-language statement
Strict comparison of Padic.mulValuation matches strict comparison of the norm.
Source project: Class Field Theory
Person-level attribution pending.