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 filtersAbstractHeckeOperator.eq_finsum_quotient_out_of_bijOn'
Plain-language statement
If a is fixed by V then ∑ᶠ g ∈ s, g • a is independent of the choice s of coset representatives in G for a subset of G ⧸ V
Source project: Fermat's Last Theorem
Person-level attribution pending.
CommGroup.no_compact_automorphisms
Plain-language statement
A connected compact Hausdorff abelian topological group does not admit a nontrivial compact group of automorphisms.
Source project: Fermat's Last Theorem
Person-level attribution pending.
FermatLastTheorem.of_p_ge_5
Plain-language statement
If Fermat's Last Theorem is true for primes p ≥ 5, then FLT is true.
Source project: Fermat's Last Theorem
Person-level attribution pending.
FiniteAdeleRing.Aux.f_g_local_global
Plain-language statement
A diagram which obviously commutes, commutes.
Source project: Fermat's Last Theorem
Person-level attribution pending.
FreyCurve.j_valuation_of_bad_prime
Plain-language statement
The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is a prime of bad reduction.
Source project: Fermat's Last Theorem
Person-level attribution pending.
FreyPackage.of_not_FermatLastTheoremFor_p_ge_5
Plain-language statement
Given a counterexample a^p+b^p=c^p to Fermat's Last Theorem with p>=5 and prime, there exists a Frey package.
Source project: Fermat's Last Theorem
Person-level attribution pending.