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.exists_adicValued_sub_lt_of_adicCompletionInteger
Plain-language statement
An element of πͺ_v can be approximated by an element of A.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.exists_forall_adicValued_sub_lt
Plain-language statement
An element of β_{v β s} πͺ_v, with s finite, can be approximated by an element of A.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.Extension.finite
Plain-language statement
There are only finitely many nonzero primes of B above a nonzero prime of A.
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.intValuation_comap
Plain-language statement
If w | v then for a β A we have w(a)=v(a)^e where e is the ramification index.
Source project: Fermat's Last Theorem
Person-level attribution pending.