Standalone Lean project
A large collaborative project formalizing the mathematics needed to prove Fermat's Last Theorem.
Flagship declarations
AbstractHeckeOperator.eq_finsum_quotient_out_of_bijOn'
Plain-language statement
If a is fixed by V then ∑ᶠ g ∈ s, g • a is independent of the choice s of coset representatives in G for a subset of G ⧸ V
Source project: Fermat's Last Theorem
Person-level attribution pending.
CommGroup.no_compact_automorphisms
Plain-language statement
A connected compact Hausdorff abelian topological group does not admit a nontrivial compact group of automorphisms.
Source project: Fermat's Last Theorem
Person-level attribution pending.
FermatLastTheorem.of_p_ge_5
Plain-language statement
If Fermat's Last Theorem is true for primes p ≥ 5, then FLT is true.
Source project: Fermat's Last Theorem
Person-level attribution pending.
FiniteAdeleRing.Aux.f_g_local_global
Plain-language statement
A diagram which obviously commutes, commutes.
Source project: Fermat's Last Theorem
Person-level attribution pending.
FreyCurve.j_valuation_of_bad_prime
Plain-language statement
The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is a prime of bad reduction.
Source project: Fermat's Last Theorem
Person-level attribution pending.
FreyPackage.of_not_FermatLastTheoremFor_p_ge_5
Plain-language statement
Given a counterexample a^p+b^p=c^p to Fermat's Last Theorem with p>=5 and prime, there exists a Frey package.
Source project: Fermat's Last Theorem
Person-level attribution pending.
Project index
Showing 8 of 85 additional declarations. Use project search for the complete index.
Group.totallyDisconnected_of_pow_prime_eq_one
Plain-language statement
A compact Hausdorff vector space over 𝔽_p is totally disconnected.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsArithFrobAt.exists_of_isInvariant_of_profinite
Plain-language statement
Let G be a finite group acting on S, and R be the fixed subring. If Q is a prime of S with finite residue field, then there exists a Frobenius element σ : G at Q.
Source project: Fermat's Last Theorem
Person-level attribution pending.
IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent_apply
Plain-language 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
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.