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 6 research declarations. Search 10,000 more complete Mathlib declarations.
6 results
Clear filtersIsDedekindDomain.HeightOneSpectrum.closureAlgebraMapIntegers_eq_integers
Plain-language statement
The closure of A in K_v is 𝒪_v.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.closureAlgebraMapIntegers_eq_prodIntegers
Plain-language statement
The closure of A in ∏_{v ∈ s} K_v is ∏_{v ∈ s} 𝒪_v. s may be infinite.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.denseRange_of_prodAlgebraMap
Plain-language 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
Plain-language 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
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.