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 filtersexists_nice_factorization
Plain-language statement
Proposition 2.5. The bulk of the proof is in the section NiceFactorization.
Source project: ABC Exceptions
Person-level attribution pending.
exists_nice_factorization'
Plain-language statement
Some basic consequences of Proposition 2.5, phrased in a way that make them more useful in the proof of Proposition 2.6.
Source project: ABC Exceptions
Person-level attribution pending.
exists_valuation_algebraMap_eq_valuation_pow
Plain-language statement
Andrew's Lemma : Density for algebraic extensions.
Source project: Class Field Theory
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.
FltRegular.caseI_easier
Plain-language statement
Case I with additional assumptions.
Source project: FLT for regular primes
Person-level attribution pending.