therefore
Sign up
Open navigation

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

1 topic

4 results

Clear filters
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