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.TateCurve
• FLT.Data.Hurwitz
• FLT.Data.QHat
• FLT.Assumptions.Mazur
• FLT.Assumptions.Odlyzko
• FLT.Deformations.Lemmas
• FLT.Deformations.Subfunctor
• FLT.GroupScheme.FiniteFlat
• FLT.NumberField.DiscriminantBounds
• FLT.Patching.Utils.Lemmas
• FLT.Patching.Utils.TopologicallyFG
• FLT.Patching.Utils.Depth
• FLT.Patching.Utils.InverseLimit
• FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract
• FLT.Deformations.ContinuousRepresentation.IsTopologicalModule
• FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete
• FLT.Deformations.Algebra.InverseLimit.Basic
• FLT.Mathlib.Algebra.IsDirectLimit
• FLT.Mathlib.Algebra.IsQuaternionAlgebra
• FLT.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
• FLT.Mathlib.Topology.Homeomorph
  • refactor: deprecate ContinuousLinearMapClass #18748
  • refactor: deprecate LinearIsometryClass #18755
  • chore: fix some explicitVarOfIff linter errors #32095
• FLT.Mathlib.Topology.Polish
• FLT.Mathlib.Topology.HomToDiscrete
• FLT.Mathlib.RepresentationTheory.Basic
• FLT.Mathlib.LinearAlgebra.Pi
  • feat(LinearAlgebra/Contraction): bijectivity of dualTensorHom + generalize to CommSemiring #25284
  • chore: prefer Pi.single i 1 j over fun j => if i = j then 1 else 0 #31949
• FLT.Mathlib.LinearAlgebra.Countable
• FLT.Mathlib.GroupTheory.Index
  • chore(Data/Quot): deprecate ind*' APIs #16314
  • feat(Algebra): additivize Dvd and Prime #27936
  • feat(MonoidAlgebra): criteria for single to be a unit, irreducible or prime #27950
• FLT.Mathlib.RingTheory.LocalRing.Defs
• FLT.Mathlib.RingTheory.Valuation.ValuationSubring
  • chore: remove CovariantClass and ContravariantClass #13124
  • chore: deprecate LinearOrderedComm{Monoid, Group}WithZero #23621
  • chore: rename field inf to min in Lattice #24614
  • fix: deprecate IsTotal in favour of Std.Total #30855
  • refactor: remove order instances from SetLike #32984
• FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation
  • feat: the adele ring of a number field is locally compact #21853
  • feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition #25991
  • feat(RingTheory/Ideal/Span): add pair lemmas #25992
  • refactor: make Valuation.Completion a def and refactor more of AdicValuation.lean #27972
  • feat : v.adicCompletionIntegers K is compact when K is a number field #30579
  • feat: localizations of primes in Dedekind domains are valuation subrings #33010
  • feat: nontrivial instances for valuation with ℤᵐ⁰ as codomain #33060
• FLT.Mathlib.RingTheory.Localization.BaseChange
  • refactor(Algebra/Module/LocalizedModule): Redefine LocalizedModule in terms of OreLocalization. #13156
  • refactor(Algebra/Module): Redefine LocalizedModule in terms of OreLocalization #19520
  • chore: unify LocalizedModule and OreLocalization #31862
• FLT.Mathlib.RingTheory.TensorProduct.Pi
  • refactor(Algebra/Algebra/Equiv): allow for non-unital AlgEquiv #29354
• FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
  • feat(Algebra): maximal Cohen Macaulay module #29533
  • feat(RingTheory): ringKrullDim of quotient via supportDim #29937
• FLT.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
  • feat: check indentation in doc-strings, medium version #27996
  • chore: redefine Ideal.IsPrime #31595
• FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
  • feat: adicCompletion for Rat is uniform isomorphic to Padic #30576
  • chore: redefine Ideal.IsPrime #31595
• FLT.Mathlib.NumberTheory.Padics.PadicIntegers
  • chore: remove global Quotient.mk ⟦·⟧ notation #17127
  • feat(RingTheory/DividedPowers/Basic): add divided power structure on pZp #26956
  • feat : v.adicCompletionIntegers K is compact when K is a number field #30579
  • refactor(Analysis/Normed/{Group/Field}/Basic): Let extends generate the repeated fields #9642
• FLT.Mathlib.NumberTheory.NumberField.Basic
  • feat(NumberTheory): every number field has a ramified prime #30666
  • feat: Various instances regarding 𝓞 K. #9444
• FLT.Mathlib.NumberTheory.NumberField.Completion
  • feat: dimensions of completions at infinite place extensions #27980
• FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
  • Development branch (2) #26138
  • feat: weak approximation theorems for infinite places of a number field #27971
• FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion
  • chore: fix def naming isses in Normed/Field/WithAbs.lean #29933
  • feat(Field/WithAbs): the lift of a ring homomorphism from WithAbs v to WithAbs w to their completions #29934
  • feat(InfinitePlace/Completion): embeddings of w.Completion factor through embeddings of v.Completion when w extends v #29942
  • feat: dimension formulae for infinite places above #30551
• FLT.Mathlib.Algebra.Algebra.Tower
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • chore(RingTheory/Ideal): make RingHom.ker take a RingHom instead of RingHomClass #25138
  • chore(Mathlib): replace => by ↦ #28622
  • refactor(Algebra/Algebra/Equiv): allow for non-unital AlgEquiv #29354
  • chore(Algebra): replace NoZeroSMulDivisors with Module.IsTorsionFree #30563
  • refactor: rename MulAction to MonoidAction #32737
  • chore(Algebra): fix whitespace #32906
  • chore: use open scoped #4960
• FLT.Mathlib.Algebra.Algebra.Hom
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • chore(RingTheory/Ideal): make RingHom.ker take a RingHom instead of RingHomClass #25138
  • chore(FreeAbelianGroup): deprecate multiplication #27759
  • chore(Mathlib): replace => by ↦ #28622
  • 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.Basic
• FLT.Mathlib.Algebra.Module.LinearMap.Defs
  • refactor: deprecate DistribMulActionSemiHomClass MulSemiringActionSemiHomClass #18756
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • feat(RingTheory/GradedAlgebra): homogeneous relation #27307
  • refactor: rename MulAction to MonoidAction #32737
• FLT.Mathlib.Algebra.Module.Submodule.Basic
  • chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables #24285
  • chore(Algebra): replace NoZeroSMulDivisors with Module.IsTorsionFree #30563
  • refactor: rename MulAction to MonoidAction #32737
  • chore: remove May 2025 deprecated declarations #33014
  • feat(gcongr): beef up @[gcongr] tag to accept ↔ & any argument order #33025
  • chore: use open scoped #4960
  • fix: deduplicate variables #6079
• FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic
  • fix: restrict abv positivity extension to variable functions #32795
• FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
• FLT.Mathlib.Topology.Algebra.Monoid
  • chore(Topology): replace continuity -> fun_prop #13994
  • chore: fix some explicitVarOfIff linter errors #32095
• FLT.Mathlib.Topology.Algebra.MulAction
  • feat: affinespace homeomorphism #22583
• FLT.Mathlib.Topology.Instances.Matrix
  • chore: replace every usage of ⬝ᵥ (with old \cdot) by ·ᵥ (with \centerdot) #27399
  • fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) #27403
• FLT.Mathlib.Topology.Algebra.Module.FiniteDimension
  • refactor: deprecate ContinuousLinearMapClass #18748
  • refactor: deprecate LinearIsometryClass #18755
• FLT.Mathlib.Topology.Algebra.Module.Quotient
• FLT.Mathlib.Topology.Algebra.Group.Units
• FLT.Mathlib.Topology.Algebra.Group.Quotient
  • feat: group markings #19475
  • refactor(Normed/Group/Quotient): generalise to non-abelian groups #21342
• FLT.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] K and 𝒪[K] 𝒪[K] #24627
  • feat(TopologyValued): Valued based on a range topology #27314
• 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): Valued based on a range topology #27314
  • refactor: make Valuation.Completion a def and refactor more of AdicValuation.lean #27972
  • feat: adicCompletion for Rat is uniform isomorphic to Padic #30576
  • feat : v.adicCompletionIntegers K is compact when K is a number field #30579
• FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic
• FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace
• FLT.Mathlib.Order.Filter.Cofinite
  • feat: express filter as supremum of principal filter and free filter #31242
  • feat: functions with finite fibers #6449
• FLT.Mathlib.MeasureTheory.Haar.Extension
• FLT.Mathlib.MeasureTheory.Group.Action
  • chore: migrate to tfae block tactic #11003
  • feat: check indentation of doc-strings, basic version #27898
  • feat: check indentation in doc-strings, medium version #27996
• FLT.Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
• FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite
  • chore: make finiteness a default tactic #26090
  • feat(Tactic/Push): add basic tags and tests #29000
• FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing
• FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct
• FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic
• FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion
• FLT.Mathlib.Data.Set.Prod
  • refactor(Finset): redefine Finset.diag, review API #11617
  • refactor: make Set.mem_graphOn defeq #18861
  • 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(Data/Set/Image): move BooleanAlgebra material to Order #26777
  • chore: fix links #27709
  • feat(Tactic/Push): add basic tags and tests #29000
  • tracking: #30658 split into pieces #30686
• FLT.Mathlib.Data.Set.Countable
• FLT.Mathlib.Data.Real.Archimedean
  • feat(Tactic/Push): add basic tags and tests #29000
  • feat: define ∃ x > y, ... notation to mean ∃ x, y < x ∧ ... #32985
  • feat: stdPart x = sSup {r | r < x} #33007
• FLT.Mathlib.Data.Fin.Basic
  • feat(MvPolynomial/Equiv): Add MvPolynomial.finSuccEquivNth #19467
  • feat: Clone and some instances #20051
  • feat: Definition of Clone #23460
  • feat: check indentation of doc-strings #27897
  • feat: check indentation of doc-strings, basic version #27898
  • feat: check indentation in doc-strings, medium version #27996
  • Lean pr testing 11156 #31587
  • chore: remove [NeZero n] assumptions in lemmas about Fin n #33079
  • feat: add Qq wrappers for ToExpr #5952
• FLT.Mathlib.LinearAlgebra.Span.Defs
  • feat(RingTheory): Picard group of a domain is isomorphic to ClassGroup #30736
  • feat(Counterexamples): invertible module not isomorphic to any ideal #32027
  • feat(RingTheory): prerequisites for #30736 #33095
• FLT.Mathlib.LinearAlgebra.TensorProduct.Basis
  • feat(LinearAlgebra/{TensorProductBasis,Dual}): basis and dual of PiTensorProduct #11156
• FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
• FLT.NumberField.InfinitePlace.Extension
• FLT.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.GLnDefs 2 sorries
• FLT.Assumptions.KnownIn1980s 2 sorries