Upstreaming dashboard
Files ready to upstream
The following files are sorry-free and do not depend on any other files, meaning they can be readily PRed to Mathlib.
FLT.TateCurve.TateCurveFLT.Data.HurwitzFLT.Data.QHatFLT.Assumptions.MazurFLT.Assumptions.OdlyzkoFLT.Deformations.LemmasFLT.Deformations.SubfunctorFLT.GroupScheme.FiniteFlatFLT.NumberField.DiscriminantBoundsFLT.Patching.Utils.LemmasFLT.Patching.Utils.TopologicallyFGFLT.Patching.Utils.DepthFLT.Patching.Utils.InverseLimitFLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.AbstractFLT.Deformations.ContinuousRepresentation.IsTopologicalModuleFLT.Deformations.RepresentationTheory.ContinuousSMulDiscreteFLT.Deformations.Algebra.InverseLimit.BasicFLT.Mathlib.Algebra.IsDirectLimitFLT.Mathlib.Algebra.IsQuaternionAlgebraFLT.Mathlib.Topology.Bases- style: replace preimage_val with ↓∩ notation #12418
- feat: restore some explicit binders from Lean 3 #24100
- chore: fix some explicitVarOfIff linter errors #32095
- feat(Topology/Sets): basis of
(Nonempty)Compacts#34266 - feat(Topology/Sets): second-countability of
(Nonempty)Compacts#34271 - feat(Topology/Sets): finite sets are dense in
(Nonempty)Compacts#34273 - feat(Topology/Sets): connectedness of
NonemptyCompacts#34278 - feat(Topology/Sets): local connectedness of
(Nonempty)Compacts#34280 - feat(Topology/Separation): add weakly first countable spaces #34894
FLT.Mathlib.Topology.PolishFLT.Mathlib.Topology.HomToDiscreteFLT.Mathlib.RepresentationTheory.BasicFLT.Mathlib.LinearAlgebra.Pi- feat(LinearAlgebra/Contraction): bijectivity of
dualTensorHom+ generalize to CommSemiring #25284 - chore: prefer
Pi.single i 1 joverfun j => if i = j then 1 else 0#31949 - feat(ContinuousMultilinearMap): generalize some definitions #34491
- feat(ContinuousAlternatingMap): generalize some definitions #34513
- feat(LinearAlgebra/Contraction): bijectivity of
FLT.Mathlib.LinearAlgebra.CountableFLT.Mathlib.GroupTheory.IndexFLT.Mathlib.RingTheory.LocalRing.DefsFLT.Mathlib.RingTheory.Valuation.ValuationSubring- chore: remove
CovariantClassandContravariantClass#13124 - chore: deprecate
LinearOrderedComm{Monoid, Group}WithZero#23621 - feat(ValuationSubring): simp lemmas for idealOfLE/ofPrime in relation to top/bot #33631
- feat(ValuationSubring): eq_self_or_eq_top_of_le #33634
- feat: abbrev for
Std.Total (· ≤ ·)#34188
- chore: remove
FLT.Mathlib.RingTheory.SimpleRing.TensorProductFLT.Mathlib.RingTheory.DedekindDomain.AdicValuation- feat: the adele ring of a number field is locally compact #21853
- feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition #25991
- refactor: make
Valuation.Completionadefand refactor more ofAdicValuation.lean#27972 - feat :
v.adicCompletionIntegers Kis compact whenKis a number field #30579 - feat: localizations of primes in Dedekind domains are valuation subrings #33010
- feat:
algebraMap K Lis uniform continuous with respect to adic topologies, when the idealwofLlies abovev#34045 - refactor: use 1-field structure to define the
WithValtype synonym #34049
FLT.Mathlib.RingTheory.Localization.BaseChangeFLT.Mathlib.RingTheory.TensorProduct.PiFLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.BasicFLT.Mathlib.RingTheory.Ideal.Quotient.Basic- chore(Data/Quot): deprecate
ind*'APIs #16314 - feat: the adele ring of a number field is locally compact #21853
- feat: the ring of integers of a
ℤₘ₀-valued field is compact whenever it is a DVR and the residue field is finite #27973 - chore: redefine
Ideal.IsPrime#31595 - feat(RingTheory): add the class
HasFiniteQuotients#35530
- chore(Data/Quot): deprecate
FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas- feat :
v.adicCompletionIntegers Kis compact whenKis a number field #30579 - chore: redefine
Ideal.IsPrime#31595 - feat: classical “decidability” instances on sets and ideals #33757
- feat:
algebraMap K Lis uniform continuous with respect to adic topologies, when the idealwofLlies abovev#34045 - refactor(Algebra): weaken NormalizationMonoid #34179
- refactor: make
OrderIso.ofHomInvtake actualOrderHoms instead of using classes #35266 - feat(Ringtheory/DedekindDomain): add RingEquiv lemmas #35532
- feat(RingTheory/DedekindDomain/Ideal/Lemmas): add nontrivial_heightOneSpectrum #35533
- feat(DedekindDomain/Factorization): add
iInfversion offinprod_heightOneSpectrum_factorization#35539
- feat :
FLT.Mathlib.NumberTheory.Padics.PadicIntegersFLT.Mathlib.NumberTheory.NumberField.CompletionFLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic- Development branch (2) #26138
- feat: weak approximation theorems for infinite places of a number field #27971
- feat(InfinitePlace/Completion): embeddings of
w.Completionfactor through embeddings ofv.Completionwhenwextendsv#29942 - refactor: use 1-field structure to define the
WithAbstype synonym #34230 - refactor: change definition of distance in normed group #35037
FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion- chore: fix
defnaming isses inNormed/Field/WithAbs.lean#29933 - feat(Field/WithAbs): the lift of a ring homomorphism from
WithAbs vtoWithAbs wto their completions #29934 - feat(InfinitePlace/Completion): embeddings of
w.Completionfactor through embeddings ofv.Completionwhenwextendsv#29942 - feat: dimension formulae for infinite places above #30551
- refactor: use 1-field structure to define the
WithAbstype synonym #34230
- chore: fix
FLT.Mathlib.Algebra.Algebra.Hom- chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
- chore(RingTheory/Ideal): make
RingHom.kertake aRingHominstead ofRingHomClass#25138 - chore(FreeAbelianGroup): deprecate multiplication #27759
- chore(Mathlib): replace
=>by↦#28622 - feat: some lemmas about AlgHom 1 and * #34238
- chore: use
open scoped#4960 - refactor: Use flat structures for morphisms #6791
- chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom #9564
FLT.Mathlib.Algebra.FixedPoints.BasicFLT.Mathlib.Algebra.Central.TensorProductFLT.Mathlib.Algebra.Module.Submodule.BasicFLT.Mathlib.Algebra.Order.AbsoluteValue.BasicFLT.Mathlib.Topology.Algebra.ContinuousAlgEquivFLT.Mathlib.Topology.Algebra.MonoidFLT.Mathlib.Topology.Algebra.MulActionFLT.Mathlib.Topology.Instances.MatrixFLT.Mathlib.Topology.Algebra.Module.FiniteDimensionFLT.Mathlib.Topology.Algebra.Module.QuotientFLT.Mathlib.Topology.Algebra.Group.UnitsFLT.Mathlib.Topology.Algebra.Group.QuotientFLT.Mathlib.Topology.Algebra.Valued.ValuationTopology- fix(Topology/Algebra/Valued): repair definition of Valued #14752
- chore: deprecate
LinearOrderedComm{Monoid, Group}WithZero#23621 - feat(Topology/Algebra/Valued):
IsLinearTopology 𝒪[K] Kand𝒪[K] 𝒪[K]#24627 - feat(TopologyValued):
Valuedbased on a range topology #27314 - refactor: change definition of distance in normed group #35037
FLT.Mathlib.Topology.Algebra.Valued.WithVal- feat(NumberTheory/Padics): the completion of
ℚat a finite place isℚ_[p]#21950 - chore: deprecate
LinearOrderedComm{Monoid, Group}WithZero#23621 - feat(TopologyValued):
Valuedbased on a range topology #27314 - refactor: make
Valuation.Completionadefand refactor more ofAdicValuation.lean#27972 - feat :
v.adicCompletionIntegers Kis compact whenKis a number field #30579 - feat:
algebraMap K Lis uniform continuous with respect to adic topologies, when the idealwofLlies abovev#34045 - refactor: use 1-field structure to define the
WithValtype synonym #34049
- feat(NumberTheory/Padics): the completion of
FLT.Mathlib.Topology.Algebra.RestrictedProduct.BasicFLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlaceFLT.Mathlib.Order.Filter.CofiniteFLT.Mathlib.MeasureTheory.Haar.ExtensionFLT.Mathlib.MeasureTheory.Group.ActionFLT.Mathlib.MeasureTheory.Measure.Typeclasses.FiniteFLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRingFLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProductFLT.Mathlib.MeasureTheory.Constructions.BorelSpace.PadicFLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletionFLT.Mathlib.Data.Set.Prod- refactor(Finset): redefine Finset.diag, review API #11617
- chore(Data/Set/Prod, SetTheory/ZFC/Basic): add theorem prod_subset_of_prod and extend ZFC model #25483
- feat(SetTheory/ZFC/Booleans): define Boolean algebra in ZFC #25484
- feat(SetTheory/ZFC/Naturals): define natural numbers in ZFC #25485
- feat(SetTheory/ZFC/Integers): define integers in ZFC #25486
- feat(SetTheory/ZFC/Rationals): define rationals in ZFC #25488
- feat(Topology/Compactness/CompactSystem): set system of finite unions of sets in a compact system is again a compact system #25900
- feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. #25902
- feat(MeasureTheory): finite unions of sets in a semi-ring (in terms of measure theory) form a ring #25903
- feat(Topology/Compactness/CompactSystem): closed and compact square cylinders form a compact system #25906
- chore: fix links #27709
- feat(Tactic/Push): add basic tags and tests #29000
FLT.Mathlib.Data.Set.CountableFLT.Mathlib.Data.Real.Archimedean- feat(Tactic/Push): add basic tags and tests #29000
- chore: use
IsLUBIsGLBinCompleteLatticeConditionallyCompleteLattice#35328 -
[ feat(NumberTheory/Height/Basic): add {mul log}Height_comp_le, {mul log}Height_fun_mul_eq #35408](https://github.com/leanprover-community/mathlib4/pull/35408)
FLT.Mathlib.Data.Fin.BasicFLT.Mathlib.LinearAlgebra.Matrix.TransvectionFLT.Mathlib.LinearAlgebra.TensorProduct.BasisFLT.Mathlib.LinearAlgebra.TensorProduct.AlgebraFLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFreeFLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.DefsFLT.NumberField.InfinitePlace.ExtensionFLT.DedekindDomain.FiniteAdeleRing.TensorPi
Files easy to unlock
The following files do not depend on any other FLT file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.
FLT.GlobalLanglandsConjectures.GLnDefs2 sorriesFLT.Assumptions.KnownIn1980s2 sorries