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,417 to 1,422 of 2,569 results.
IsDedekindDomain.HeightOneSpectrum.denseRange_of_prodAlgebraMap
Mathematical statement
If s is finite then K in dense in ∏_{v ∈ s} K_v.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.exists_adicValued_mul_sub_le
Mathematical statement
Given a, b ∈ A and v b ≤ v a we can find y in A such that y is close to a / b by the valuation v.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.exists_adicValued_sub_lt_of_adicCompletionInteger
Mathematical 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
Mathematical 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
Mathematical 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
Mathematical statement
The range of adicCompletionIntegers.tensorToAdicCompletion is 𝓞_w.
Source project: Fermat's Last Theorem
Person-level attribution pending.