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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,783 to 1,788 of 2,569 results.
NumberField.AdeleRing.units_mem_ringHaarCharacter_ker
Mathematical 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
Mathematical 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
Mathematical 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.
Obelix.PartialSolution.DFinsuppInfinite_not_Finite
Mathematical statement
The module Π₀ _ : ℕ, ℤ is not a finite rank module over ℤ
Source project: Equational Theories
Person-level attribution pending.
ofReal_tvDist_bind_left_le_const
Mathematical statement
ℝ≥0∞ form of tvDist_bind_left_le_const, matching the quantitative APIs: a per-a bound ENNReal.ofReal (tvDist (f a) (g a)) ≤ ε on the support of mx lifts through the shared bind.
Source project: VCVio
Person-level attribution pending.
omega_reg_lang_fin_idx_congr
Mathematical statement
If a congruence is of finite index, is ample, and saturates an ω-language L, then L is ω-regular.
Source project: Automata Theory
Person-level attribution pending.