Login

ImperialCollegeLondon/FLT

maintenance drain
main public updated latest build queued
4771 checked 0 blocked 0 open 1 queued last run

Next action Worker drain enabled Verification is queued while maintenance drain is pausing new claims. Latest error: job_failed
Theorems · 4771 tracked
Indexed 4771 theorem-like declarations
Sorries left 1% 32 markers in 31 declarations
Blueprint 67 nodes to go
182 of 249 proved 29 ready 27 blocked 11 draft

Showing 200 theorems.

Theorem Status Owner Module Last run
absolutelyIrreducible Checked unowned FLT/Deformations/RepresentationTheory/Irreducible.lean
add_apply Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/Defs.lean
add_comm_of_disjoint_support Checked unowned FLT/Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean
add_def Checked unowned FLT/Deformations/Algebra/InverseLimit/Basic.lean
addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv Checked unowned FLT/HaarMeasure/HaarChar/AddEquiv.lean
addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding Checked unowned FLT/HaarMeasure/HaarChar/AddEquiv.lean
addEquivAddHaarChar_eq_ringHaarChar_det Checked unowned FLT/HaarMeasure/HaarChar/FiniteDimensional.lean
addEquivAddHaarChar_eq_ringHaarChar_det_diagonal Checked unowned FLT/HaarMeasure/HaarChar/FiniteDimensional.lean
addEquivAddHaarChar_eq_ringHaarChar_det_matrix_pi Checked unowned FLT/HaarMeasure/HaarChar/FiniteDimensional.lean
addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc Checked unowned FLT/HaarMeasure/HaarChar/FiniteDimensional.lean
addEquivAddHaarChar_eq_ringHaarChar_det_pi Checked unowned FLT/HaarMeasure/HaarChar/FiniteDimensional.lean
addEquivAddHaarChar_map_open Checked unowned FLT/HaarMeasure/HaarChar/AddEquiv.lean
addEquivAddHaarChar_mulRight_unit_eq_one Checked unowned FLT/HaarMeasure/HaarChar/AdeleRing.lean
addEquivAddHaarChar_piCongrRight Checked unowned FLT/HaarMeasure/HaarChar/AddEquiv.lean
addEquivAddHaarChar_prodCongr Checked unowned FLT/HaarMeasure/HaarChar/AddEquiv.lean
addEquivAddHaarChar_restrictedProductCongrRight Checked unowned FLT/HaarMeasure/HaarChar/AddEquiv.lean
addEquivAddHaarChar_restrictedProductCongrRight_of_principal Checked unowned FLT/HaarMeasure/HaarChar/AddEquiv.lean
add_fst Checked unowned FLT/Mathlib/NumberTheory/NumberField/AdeleRing.lean
addHaarScalarFactor_tensor_adeles_eq_one Checked unowned FLT/HaarMeasure/HaarChar/AdeleRing.lean
addHaarScalarFactor_tensor_adeles_rat_eq_one Checked unowned FLT/HaarMeasure/HaarChar/AdeleRing.lean
add_im_i Checked unowned FLT/Data/Hurwitz.lean
add_im_o Checked unowned FLT/Data/Hurwitz.lean
add_im_oi Checked unowned FLT/Data/Hurwitz.lean
add_re Checked unowned FLT/Data/Hurwitz.lean
add_snd Checked unowned FLT/Mathlib/NumberTheory/NumberField/AdeleRing.lean
adicCompletionSemialgHom_coe Checked unowned FLT/DedekindDomain/Completion/BaseChange.lean
adicCompletionSemialgHom_continuous Checked unowned FLT/DedekindDomain/Completion/BaseChange.lean
adicCompletionSemialgHom_image_adicCompletionIntegers Checked unowned FLT/DedekindDomain/Completion/BaseChange.lean
adicCompletionUniformizer_ne_zero Checked unowned FLT/DedekindDomain/FiniteAdeleRing/LocalUnits.lean
adicCompletionUniformizer_spec Checked unowned FLT/DedekindDomain/FiniteAdeleRing/LocalUnits.lean
adjoin_adjoin_right Checked unowned FLT/Deformations/Lemmas.lean
algebraMap_apply Checked unowned FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
algebraMap_apply Checked unowned FLT/Mathlib/Algebra/Algebra/Hom.lean
algebraMap_apply_eq_algebraMap Checked unowned FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
algebraMap_bijective Checked unowned FLT/Deformations/IsResidueAlgebra.lean
algebraMap_completion Checked unowned FLT/DivisionAlgebra/Finiteness.lean
algebraMap_completion_def Checked unowned FLT/DivisionAlgebra/Finiteness.lean
algebraMap_completionIntegers Checked unowned FLT/DedekindDomain/AdicValuation.lean
algebraMap_continuous Checked unowned FLT/Patching/Algebra.lean
algebraMap_def Checked unowned FLT/Deformations/Lemmas.lean
algebraMap_eval Checked unowned FLT/Hacks/RightActionInstances.lean
algebraMap_surjective Checked unowned FLT/Deformations/IsResidueAlgebra.lean
algebraMap_surjective Checked unowned FLT/Patching/Algebra.lean
algebra_ringHaarChar_eq_ringHaarChar_det Checked unowned FLT/HaarMeasure/HaarChar/FiniteDimensional.lean
algHomEquivOfIsDomain_apply_fst Checked unowned FLT/Deformations/RepresentationTheory/Etale.lean
algHomEquivOfIsDomain_apply_snd_apply Checked unowned FLT/Deformations/RepresentationTheory/Etale.lean
algHomEquivOfIsDomain_symm_apply_apply Checked unowned FLT/Deformations/RepresentationTheory/Etale.lean
almost_always_bijOn Checked unowned FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean
almost_always_mapsTo Checked unowned FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean
antidiag_mem_C Checked unowned FLT/DivisionAlgebra/Finiteness.lean
apply_mem_integer Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Local.lean
apply_one_one_notMem_maximalIdeal Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Local.lean
apply_one_zero_mem_maximalIdeal Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Local.lean
apply_zero_zero_sub_apply_one_one_mem_maximalIdeal Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Local.lean
arithFrobAt' Checked unowned FLT/Deformations/RepresentationTheory/Frobenius.lean
aux Checked unowned FLT/Data/Hurwitz.lean
aux2 Checked unowned FLT/Data/Hurwitz.lean
b₂ Checked unowned FLT/FreyCurve/FreyPackage.lean
b₄ Checked unowned FLT/FreyCurve/FreyPackage.lean
baseChangeAdeleAlgHom_bijective Checked unowned FLT/NumberField/AdeleRing.lean
baseChangeAlgEquiv_apply Checked unowned FLT/NumberField/AdeleRing.lean
baseChangeAlgEquiv_fst_apply Checked unowned FLT/NumberField/AdeleRing.lean
baseChangeAlgEquiv_snd_apply Checked unowned FLT/NumberField/AdeleRing.lean
baseChangeAlgEquiv_tmul Checked unowned FLT/NumberField/InfiniteAdeleRing.lean
baseChange_apply Checked unowned FLT/HaarMeasure/HaarChar/AdeleRing.lean
baseChange_apply Checked unowned FLT/NumberField/InfiniteAdeleRing.lean
baseChange_bijective Checked unowned FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
baseChange_bijective Checked unowned FLT/DedekindDomain/Completion/BaseChange.lean
baseChange_comp Checked unowned FLT/Hacks/RightActionInstances.lean
baseChange_def Checked unowned FLT/Deformations/RepresentationTheory/GaloisRep.lean
baseChangeEquiv_tmul Checked unowned FLT/NumberField/Completion/Infinite.lean
baseChangeEquiv_tsum_apply_right Checked unowned FLT/NumberField/AdeleRing.lean
baseChange_existsListTransvecEtc Checked unowned FLT/Mathlib/LinearAlgebra/Matrix/Transvection.lean
baseChange_fst_apply Checked unowned FLT/NumberField/AdeleRing.lean
baseChange_GL Checked unowned FLT/Deformations/RepresentationTheory/GaloisRep.lean
baseChange_id Checked unowned FLT/Hacks/RightActionInstances.lean
baseChange_injective Checked unowned FLT/NumberField/Completion/Infinite.lean
baseChangeLinearEquiv_tmul Checked unowned FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
baseChange_map Checked unowned FLT/Deformations/RepresentationTheory/GaloisRep.lean
baseChange_map Checked unowned FLT/Deformations/RepresentationTheory/GaloisRep.lean
baseChange_of_algebraMap_tmul Checked unowned FLT/Mathlib/Algebra/Algebra/Bilinear.lean
baseChange_of_algebraMap_tmul_left Checked unowned FLT/Mathlib/Algebra/Algebra/Bilinear.lean
baseChange_of_algebraMap_tmul_right Checked unowned FLT/Mathlib/Algebra/Algebra/Bilinear.lean
baseChangeRight_isOpenQuotientMap Checked unowned FLT/DedekindDomain/Completion/BaseChange.lean
baseChangeRightOfAlgebraMap_apply Checked unowned FLT/Mathlib/Algebra/Algebra/Bilinear.lean
baseChangeRightOfAlgebraMap_coe Checked unowned FLT/Mathlib/Algebra/Algebra/Bilinear.lean
baseChangeRight_surjective Checked unowned FLT/DedekindDomain/Completion/BaseChange.lean
baseChange_snd_apply Checked unowned FLT/NumberField/AdeleRing.lean
baseChange_surjective Checked unowned FLT/NumberField/Completion/Infinite.lean
baseChange_tmul Checked unowned FLT/Deformations/RepresentationTheory/GaloisRep.lean
baseChange_tmul_apply Checked unowned FLT/DedekindDomain/Completion/BaseChange.lean
basis_eq Checked unowned FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean
basis_eq_global Checked unowned FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean
basis_eq_single Checked unowned FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean
basis_eq_single_global Checked unowned FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean
basis_repr_eq Checked unowned FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean
basis_repr_eq_global Checked unowned FLT/HaarMeasure/HaarChar/FiniteAdeleRing.lean
bijective_of_eventually_bijective Checked unowned FLT/Patching/Ultraproduct.lean
bijOn_smul Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Abstract.lean
bijOn_unipotent_mul_diagU1_U1diagU1 Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Local.lean
bijOn_unipotent_mul_diagU1_U1diagU1 Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean
bounded_by Checked unowned FLT/GlobalLanglandsConjectures/GLnDefs.lean
bracketBilin_apply_apply Checked unowned FLT/GlobalLanglandsConjectures/GLnDefs.lean
c₄ Checked unowned FLT/FreyCurve/FreyPackage.lean
c₄' Checked unowned FLT/FreyCurve/FreyPackage.lean
canonicalForm Checked unowned FLT/Data/QHat.lean
canonicalForm Checked unowned FLT/Data/HurwitzRatHat.lean
card_quotient_le Checked unowned FLT/Patching/Module.lean
card_rootsOfUnity Checked unowned FLT/GaloisRepresentation/Cyclotomic.lean
castDef_negSucc Checked unowned FLT/Data/Hurwitz.lean
castDef_ofNat Checked unowned FLT/Data/Hurwitz.lean
castHom_val_modEq Checked unowned FLT/GaloisRepresentation/Cyclotomic.lean
C_compact Checked unowned FLT/DivisionAlgebra/Finiteness.lean
center_tensorProduct Checked unowned FLT/Mathlib/Algebra/Central/TensorProduct.lean
center_tensorProduct_eq_inf Checked unowned FLT/Mathlib/Algebra/Central/TensorProduct.lean
changeScalars_apply Checked unowned FLT/Mathlib/Algebra/Algebra/Tower.lean
changeScalars_apply Checked unowned FLT/Mathlib/Algebra/Algebra/Tower.lean
charFrob_eq Checked unowned FLT/Deformations/RepresentationTheory/GaloisRep.lean
charZero Checked unowned FLT/Data/QHat.lean
closureAlgebraMapIntegers_eq_integers Checked unowned FLT/DedekindDomain/AdicValuation.lean
closureAlgebraMapIntegers_eq_prodIntegers Checked unowned FLT/DedekindDomain/AdicValuation.lean
closure_nonZeroDivisors_padicInt Checked unowned FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean
cocompact Checked unowned FLT/NumberField/AdeleRing.lean
cocompact Checked unowned FLT/NumberField/AdeleRing.lean
codRestrict_comp Checked unowned FLT/Mathlib/Topology/Constructions.lean
coe_add Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Abstract.lean
coe_add Checked unowned FLT/Mathlib/Algebra/FixedPoints/Basic.lean
coe_coe Checked unowned FLT/Mathlib/Topology/Algebra/Algebra/Hom.lean
coe_coe Checked unowned FLT/Mathlib/Algebra/Algebra/Hom.lean
coe_coeRingHom Checked unowned FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean
coe_dvd_iff Checked unowned FLT/GaloisRepresentation/Cyclotomic.lean
coeHomₜ_toFun Checked unowned FLT/Deformations/Lemmas.lean
coe_inj Checked unowned FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean
coe_injective Checked unowned FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean
coe_lTensorLeft_eq_lTensor Checked unowned FLT/DedekindDomain/FiniteAdeleRing/TensorRestrictedProduct.lean
coe_mk Checked unowned FLT/Mathlib/Algebra/Algebra/Hom.lean
coe_mk Checked unowned FLT/Deformations/Lemmas.lean
coe_mulLeft Checked unowned FLT/Mathlib/Algebra/Algebra/Bilinear.lean
coe_mulRight Checked unowned FLT/Mathlib/Algebra/Algebra/Bilinear.lean
coe_norm Checked unowned FLT/Data/Hurwitz.lean
coe_of Checked unowned FLT/Deformations/Categories.lean
coe_smul Checked unowned FLT/Deformations/Lemmas.lean
coe_smul Checked unowned FLT/Deformations/Lemmas.lean
coe_smul Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Abstract.lean
coe_toContinuousMonoidHom Checked unowned FLT/Deformations/Lemmas.lean
coe_toExtension Checked unowned FLT/NumberField/InfinitePlace/Extension.lean
coe_toHomeomorph Checked unowned FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
coe_toHomeomorph Checked unowned FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
coe_zero Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Abstract.lean
cofinite_mapsTo_adicCompletionSemialgHom Checked unowned FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
comap_eq Checked unowned FLT/NumberField/InfinitePlace/Extension.lean
comap_eq Checked unowned FLT/NumberField/InfinitePlace/Extension.lean
comapHom_cont Checked unowned FLT/NumberField/Completion/Infinite.lean
comap_piEquiv_principalSubgroup Checked unowned FLT/NumberField/AdeleRing.lean
comap_smul_of_le_range Checked unowned FLT/Patching/Utils/Lemmas.lean
comap_smul_of_surjective Checked unowned FLT/Patching/Utils/Lemmas.lean
comap_smul_one Checked unowned FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean
comm Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Abstract.lean
comm_apply_tmul Checked unowned FLT/Hacks/RightActionInstances.lean
comm_apply_tmul Checked unowned FLT/Hacks/RightActionInstances.lean
comm_symm_apply_tmul Checked unowned FLT/Hacks/RightActionInstances.lean
comm_symm_apply_tmul Checked unowned FLT/Hacks/RightActionInstances.lean
commutes Checked unowned FLT/Mathlib/Topology/Algebra/Algebra/Hom.lean
commutes Checked unowned FLT/Mathlib/Algebra/Algebra/Hom.lean
commutes Checked unowned FLT/Mathlib/Algebra/Algebra/Tower.lean
compact_includeLeft_subgroup Checked unowned FLT/DivisionAlgebra/Finiteness.lean
compact_quotient Checked unowned FLT/DivisionAlgebra/Finiteness.lean
compactSpace Checked unowned FLT/Patching/Utils/Lemmas.lean
compactSpace Checked unowned FLT/Patching/Utils/AdicTopology.lean
compactSpace_of_finite_residueField Checked unowned FLT/Patching/Utils/AdicTopology.lean
comp_apply Checked unowned FLT/Deformations/Categories.lean
compatibility Checked unowned FLT/Mathlib/Algebra/IsDirectLimit.lean
compatibility' Checked unowned FLT/Mathlib/Algebra/IsDirectLimit.lean
compatibility_module Checked unowned FLT/Mathlib/Algebra/IsDirectLimit.lean
comp_def Checked unowned FLT/Mathlib/RepresentationTheory/Basic.lean
completed_units Checked unowned FLT/Data/HurwitzRatHat.lean
completionIdeal_ne_bot Checked unowned FLT/DedekindDomain/AdicValuation.lean
componentEquiv Checked unowned FLT/Patching/Algebra.lean
componentMapModule_surjective Checked unowned FLT/Patching/Module.lean
componentMapRingHom_surjective Checked unowned FLT/Patching/Algebra.lean
components_comp_coe_eq_coe_apply Checked unowned FLT/Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean
cond Checked unowned FLT/Patching/Algebra.lean
cond Checked unowned FLT/Patching/Module.lean
cond Checked unowned FLT/Deformations/RepresentationTheory/GaloisRep.lean
cond Checked unowned FLT/Patching/Module.lean
congr_simp Checked unowned FLT/Deformations/RepresentationTheory/GaloisRep.lean
congr_simp Checked unowned FLT/Mathlib/Algebra/Algebra/Tower.lean
congr_simp Checked unowned FLT/Mathlib/LinearAlgebra/Determinant.lean
congr_simp Checked unowned FLT/Mathlib/LinearAlgebra/Dimension/Constructions.lean
congr_simp Checked unowned FLT/Patching/Algebra.lean
congr_simp Checked unowned FLT/AutomorphicForm/QuaternionAlgebra/Defs.lean
congr_simp Checked unowned FLT/NumberField/AdeleRing.lean
congr_simp Checked unowned FLT/Mathlib/Topology/Algebra/RestrictedProduct/Equiv.lean
congr_simp Checked unowned FLT/NumberField/AdeleRing.lean
congr_simp Checked unowned FLT/DedekindDomain/FiniteAdeleRing/TensorRestrictedProduct.lean
congr_simp Checked unowned FLT/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean
congr_simp Checked unowned FLT/DivisionAlgebra/Finiteness.lean
congr_simp Checked unowned FLT/Deformations/RepresentationTheory/Etale.lean
congr_simp Checked unowned FLT/Deformations/LiftFunctor.lean
congr_simp Checked unowned FLT/DedekindDomain/Completion/BaseChange.lean

Showing the highest-priority 200 proofs for fast server render.

Keyboard shortcuts