Source-pinned research

Research proof index

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 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

2569 results

Project-declaredLean 4.32.0

Potential Is Stable of strong

TwoHiggsDoublet.potentialIsStable_of_strong

Project documentation

The potential is stable if it is strongly stable, i.e. its quartic term is always positive. The proof of this result relies on the compactness of the closed unit ball in EuclideanSpace ℝ (Fin 3), and the extreme value theorem.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Ultra Product continuous of bdd Above card

UltraProduct.continuous_of_bddAbove_card

Plain-language statement

Let R₀ be a topological ring, topologically of finite type (over ). Consider a family of (cardinality) finite rings R i with the discrete topology whose cardinalites are unifomly bounded. Given a family of continuous ring homs f i : R →+* R i, the lift R →+* 𝒰(Rᵢ) is also continuous.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Ultra Product exists alg Equiv of bdd Above card

UltraProduct.exists_algEquiv_of_bddAbove_card

Plain-language statement

Let R₀ be a topological ring, topologically of finite type (over ). Consider a family of (cardinality) finite continuous R₀-algebras R i with the discrete topology whose cardinalites are unifomly bounded. Then 𝒰(Rᵢ) ≃ₐ[R] R i for F-many i.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Ultra Product exists ring Equiv of bdd Above card

UltraProduct.exists_ringEquiv_of_bddAbove_card

Plain-language statement

Let R₀ be a topological ring, topologically of finite type (over ). Consider a family of (cardinality) finite rings R i with the discrete topology whose cardinalites are unifomly bounded. Given a family of continuous ring homs f i : R →+* R i, there exists F-many i such that 𝒰(Rᵢ) ≃+* R i and this map is compatible with f.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Ultra Product surjective of bdd Above card

UltraProduct.surjective_of_bddAbove_card

Plain-language statement

Let R₀ be a topological ring, topologically of finite type (over ). Consider a family of (cardinality) finite rings R i with the discrete topology whose cardinalites are unifomly bounded. Given a family of continuous surjective ring homs f i : R →+* R i, the lift R →+* 𝒰(Rᵢ) is also surjective.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record