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 91 research declarations. Search 10,000 more complete Mathlib declarations.
91 results
Clear filtersGroup.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.
IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent_apply
Plain-language statement
If Ο : πΈ_K^f β V β πΈ_K^f β V is πΈ_K^f-linear and Οβ is its local component at a place p then for all x : πΈ_K^f β V we have (evalβ β id_V) (Ο x) = Οβ ((evalβ β id_V) x), or, more colloquiually, (Ο x)β = Οβ (xβ).
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight_surjective
Plain-language statement
The canonical map L β[K] K_v β β_{w|v} L_w is surjective.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.adicCompletion.finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletion
Plain-language statement
L β[K] K_v and β_{w|v} L_w have equal dimensions
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.closureAlgebraMapIntegers_eq_integers
Plain-language statement
The closure of A in K_v is πͺ_v.
Source project: Fermat's Last Theorem
Person-level attribution pending.