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 91 research declarations. Search 10,000 more complete Mathlib declarations.
91 results
Clear filtersIsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_isClopen_range
Plain-language statement
The image of B ⊗[A] 𝓞_v in L ⊗[K] K_v is clopen.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_range_subset_closure
Plain-language statement
The image of B ⊗[A] 𝓞_v in L ⊗[K] K_v is contained in the closure of the image of B.
Source project: Fermat's Last Theorem
Person-level attribution pending.
MaximalPQuotient.isPGroup_of_isTorsion
Plain-language statement
The "maximal p-quotient" of (ℤ, +) is ℤ/⋂ₙ pⁿℤ = ℤ, not a p-group.
Source project: Fermat's Last Theorem
Person-level attribution pending.
MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_diagonal
Plain-language statement
A diagonal matrix scales addHaar with its determinant
Source project: Fermat's Last Theorem
Person-level attribution pending.
MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc
Plain-language statement
Haar measure scaling for invertible linear maps on a finite-dimensional vector space over a field F assuming [SecondCountableTopology F].
Source project: Fermat's Last Theorem
Person-level attribution pending.
MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_pi
Plain-language statement
Haar measure scaling for linear maps on (ι → F)
Source project: Fermat's Last Theorem
Person-level attribution pending.