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 95 research declarations. Search 10,000 more complete Mathlib declarations.
95 results
Clear filtersFltRegular.caseI_easier
Plain-language statement
Case I with additional assumptions.
Source project: FLT for regular primes
Person-level attribution pending.
FltRegular.caseII
Plain-language statement
Case II of Fermat's Last Theorem for regular primes.
Source project: FLT for regular primes
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.
Group.totallyDisconnected_of_pow_prime_eq_one
Plain-language statement
A compact Hausdorff vector space over 𝔽_p is totally disconnected.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsArithFrobAt.exists_of_isInvariant_of_profinite
Plain-language statement
Let G be a finite group acting on S, and R be the fixed subring. If Q is a prime of S with finite residue field, then there exists a Frobenius element σ : G at Q.
Source project: Fermat's Last Theorem
Person-level attribution pending.