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 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.
dvd_card_classGroup_of_unramified_isCyclic
Plain-language statement
This is the second part of Hilbert Theorem 94, which states that if L/K is an unramified cyclic finite extension of number fields of odd prime degree, then the degree divides the class number of K.
Source project: FLT for regular primes
Person-level attribution pending.
eq_pow_prime_of_unit_of_congruent
Plain-language statement
A regular prime criterion: if a unit of the cyclotomic field is congruent to an integer modulo p, then it is a p-th power.
Source project: FLT for regular primes
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.