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 filtersIsDedekindDomain.HeightOneSpectrum.isClosed_baseChange_image_closure_range_algebraMap
Plain-language statement
The image of B β[A] π_v (the closure of B) in β_w L_w is closed.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.range_baseChange_comp_tensorAdicCompletionTo_eq_pi
Plain-language statement
The image of B β[A] π_v in β_w L_w is β_w π_w.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.range_tensorAdicCompletionIntegersTo_eq_closure_range_algebraMap
Plain-language statement
The image of B β[A] π_v in L β[K] K_v is the closure of the image of B.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_isClopen_range
Plain-language statement
The image of B β[A] π_v in L β[K] K_v is clopen.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_range_subset_closure
Plain-language 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.
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.