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 filtersFltRegular.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.
geometryBound_set_finite
Plain-language statement
The set that we are taking the infimum over in the geometry bound is a finite set.
Source project: ABC Exceptions
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.
groupCohomology.exists_of_surjective
Plain-language statement
Given map f: M ⟶ N and q : ℕ, if H^{q+1}(M) ⟶ H^{q+1}(N) is surjective, then any z : Z^{q+1}(N) can be written as f(z') + d(y) for some z' : Z^{q+1}(M) and y : C^q(M). Note that d is spelled as toCocycles.
Source project: Class Field Theory
Person-level attribution pending.