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 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.
continuous_algebraMap_of_density
Plain-language statement
Maddy's Lemma : Density implies continuity.
Source project: Class Field Theory
Person-level attribution pending.
DeterminantBound.application
Plain-language statement
A particular application of the determinant bound used in subcase 2.1
Source project: ABC Exceptions
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.