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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,429 to 1,434 of 2,569 results.
IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_range_subset_closure
Mathematical statement
The image of B ⊗[A] 𝓞_v in L ⊗[K] K_v is contained in the closure of the image of B.
Source project: Fermat's Last Theorem
Person-level attribution pending.
isLocallyBounded_of_isCadlag
Mathematical statement
A càdlàg function is locally bounded.
Source project: Brownian motion
Person-level attribution pending.
IsNonarchimedeanLocalField.exists_pow_smul_integer_mem_span
Mathematical 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
Mathematical 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
Mathematical statement
The maximal unramified subextension is maximal.
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.nonempty_unramifiedExtension_algEquiv_of_isUnramified
Mathematical 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.