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,411 to 1,416 of 2,569 results.
IsCompactSystem.finsetCoe
Mathematical statement
The set of Finset coercions forms a compact system.
Source project: Brownian motion
Person-level attribution pending.
IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent_apply
Mathematical statement
If Ο : πΈ_K^f β V β πΈ_K^f β V is πΈ_K^f-linear and Οβ is its local component at a place p then for all x : πΈ_K^f β V we have (evalβ β id_V) (Ο x) = Οβ ((evalβ β id_V) x), or, more colloquiually, (Ο x)β = Οβ (xβ).
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight_surjective
Mathematical 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
Mathematical 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
Mathematical 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
Mathematical 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.