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 20 research declarations. Search 10,000 more complete Mathlib declarations.
20 results
Clear filtersgroupCohomology.trivialCohomology_of_even_of_odd_of_solvable
Plain-language statement
If H²ⁿ⁺²(H,M) and H²ᵐ⁺¹(H,M) are both zero for every subgroup H of G then M is acyclic.
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.exists_pow_smul_integer_mem_span
Plain-language statement
Bounded denominators: if b is any finite K-basis of L and ϖ is a uniformiser of K, then a large enough power of ϖ multiplies every integer of L into the 𝒪[K]-lattice spanned by b. This is the key analytic input both for Module.Finite 𝒪[K] 𝒪[L] (see below) and, applied to a normal basis, for the construction of an open cohomologi...
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.exists_pow_smul_mem_integer
Plain-language statement
Every element of L is carried into the integers 𝒪[L] by a large enough power of a uniformiser of K.
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.le_maximalUnramified_iff
Plain-language statement
The maximal unramified subextension is maximal.
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.nonempty_unramifiedExtension_algEquiv_of_isUnramified
Plain-language statement
If L/K is unramified, then L is isomorphic to Kn where n = [L:K].
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.nonempty_unramifiedExtension_alghom_of_dvd_f
Plain-language statement
If Kn denotes the unramified extension of K of degree n, then Kn embeds into L if n ∣ f K L. This is half of the universal property.
Source project: Class Field Theory
Person-level attribution pending.