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.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.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.