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 filtersTateCurve.valuation_evalInt_sub_sum_le
Plain-language statement
Quantitative tail bound: the evaluation of an integral power series on the open unit disc is within |q|^N of its N-th partial sum.
Source project: Fermat's Last Theorem
Person-level attribution pending.
TateCurve.weierstrass_equation
Plain-language statement
The point (X(u,q), Y(u,q)) satisfies the Weierstrass equation y² + xy = x³ + a₄x + a₆ of the Tate curve, as an identity in ℚ(u)⟦q⟧.
Source project: Fermat's Last Theorem
Person-level attribution pending.
toMatrix_f
Plain-language statement
The matrix reps of φ and f φ agree.
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.
TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.heckeOperator_eq_lTensor
Plain-language statement
Hecke operators are preserved under the identification 𝒮²(U, χ; M) ≃ M ⊗ 𝒮²(U, χ; R).
Source project: Fermat's Last Theorem
Person-level attribution pending.
TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.range_unipotentMulDiagU1
Plain-language statement
Each coset in U1diagU1 is of the form unipotent_mul_diagU1 for some t ∈ O_v.
Source project: Fermat's Last Theorem
Person-level attribution pending.