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 9 research declarations. Search 10,000 more complete Mathlib declarations.
9 results
Clear filtersIsDedekindDomain.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.Extension.tensorAdicCompletionIntegersToAdicCompletion_range_eq_integers
Plain-language statement
The range of adicCompletionIntegers.tensorToAdicCompletion is π_w.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.Extension.valued_adicCompletionSemialgHom
Plain-language statement
The local ramification index for the extension L_w/K_v is equal to the global ramification index for the extension w/v. In other words, if x in K_v and i:K_v->L_w then w(i(x))=v(x)^e where e is computed globally.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.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.