Upstreaming dashboard
Files ready to upstream
The following files are sorry-free and do not depend on any other file, meaning they can be readily PRed to Mathlib.
PRs are grouped as 'relevant' if they contain the following label: FLT
18 open pull requests (0 with relevant labels)
Other
- chore: use `open scoped` #4960
- refactor: Use flat structures for morphisms #6791
- perf: do not search algebraic hierarchy when searching `FunLike` hierarchy #17675
- feat(RingTheory/Pure): pure submodules #22909
- chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` #25138
- feat(RingTheory/GradedAlgebra): homogeneous relation #27307
- chore(Mathlib): replace `=>` by `↦` #28622
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- chore: run docstrings through mdformat #35686
- chore: override `npow` in compositional monoids #36878
- refactor(Algebra): semialgebra maps #38376
- chore(Algebra): consolidate variables and sections for `AlgHom`/`AlgEquiv` #38964
- chore(Algebra): `coe_ringHom` -> `coe_toRingHom` #38966
- chore: shake --keep-implied --keep-prefix --fix #39386
- feat(RingTheory): etale lifting property of henselian local rings #41086
- feat(FieldTheory/Minpoly): generalize theorem #42068
- refactor: rename `MulAction` to `MonoidAction` #43404
- chore: use `congr()` much more widely #43408
21 open pull requests (0 with relevant labels)
Other
- chore: use `open scoped` #4960
- refactor: Use flat structures for morphisms #6791
- perf: reorder `extends` and change instance priority in algebra hierarchy #7873
- chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom #9564
- perf: reorder `extends` and remove some instances in algebra hierarchy #16594
- perf: reorder `extends` of `(Add)Monoid` #16637
- perf: do not search algebraic hierarchy when searching `FunLike` hierarchy #17675
- refactor: deprecate `SemilinearMapClass` #18805
- chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` #25138
- chore(FreeAbelianGroup): deprecate multiplication #27759
- chore(Mathlib): replace `=>` by `↦` #28622
- chore: override `npow` in compositional monoids #36878
- feat(RingTheory/AugmentationIdeal): base change for augmentation ideals #37745
- refactor(Algebra): semialgebra maps #38376
- test(Tactic/Algebra): try to replace `ring` with algebra in many places #38637
- chore(Algebra): consolidate variables and sections for `AlgHom`/`AlgEquiv` #38964
- chore(Algebra): `coe_ringHom` -> `coe_toRingHom` #38966
- chore: shake --keep-implied --keep-prefix --fix #39386
- perf: reorder `extends` and change instance priority in algebra hierarchy #41846
- feat(FieldTheory/Minpoly): generalize theorem #42068
- chore: use `congr()` much more widely #43408
9 open pull requests (0 with relevant labels)
Other
- chore: use `open scoped` #4960
- lint also `let` vs `have` #12181
- 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: run docstrings through mdformat #35686
- chore: shake --keep-implied --keep-prefix --fix #39386
- refactor: rename `MulAction` to `MonoidAction` #43404
- chore: use `congr()` much more widely #43408
4 open pull requests (0 with relevant labels)
No open pull requests.
6 open pull requests (0 with relevant labels)
Other
- chore: remove `meta` form `import Mathlib.Tactic...` #35042
- fix: improve defeqs of comp actions #38968
- chore: specify doc-strings of auto-generated additive declarations di… #41565
- chore: add missing `to_additive` docstrings #41628
- chore: add missing `to_additive` docstrings in Algebra/Group actions and homs #41636
- refactor: rename `MulAction` to `MonoidAction` #43404
4 open pull requests (0 with relevant labels)
Other
No open pull requests.
No open pull requests.
3 open pull requests (0 with relevant labels)
3 open pull requests (0 with relevant labels)
2 open pull requests (0 with relevant labels)
5 open pull requests (0 with relevant labels)
Other
- refactor(Algebra/Group): make `IsUnit` a typeclass #17458
- chore: remove `noncomputable section` when only theorems in file #41554
- refactor(Algebra/Polynomial): make into an `abbrev` of `AddMonoidAlgebra` #41981
- feat: use `max`/`min` for `union`/`intersection` in `Set`, `Finset`, `ZFSet`, `Class` #42316
- feat(Algebra/Polynomial/Splits): specialization of `Split.of_splits_map_of_injective` to `algebraMap` #43353
8 open pull requests (0 with relevant labels)
Other
- feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition #25991
- feat(AlgebraicGeometry): add x, y, px, py for points on elliptic curves #26078
- refactor(Algebra): add type-classes for algebraic properties of `FunLike` #33477
- Nagell lutz #35863
- feat(AlgebraicGeometry/EllipticCurve): add notation and pretty printer for points #36334
- chore: replace `:= by rfl` with `:= rfl` #40381
- feat(EllipticCurve): the universal elliptic curve #41300
- refactor: unify `Set.mem_ofPred_eq` into `Set.mem_ofPred` #42692
2 open pull requests (0 with relevant labels)
2 open pull requests (0 with relevant labels)
9 open pull requests (0 with relevant labels)
Other
- feat: add Qq wrappers for ToExpr #5952
- style: Change Subtype.val to (↑) #12465
- feat(MvPolynomial/Equiv): Add `MvPolynomial.finSuccEquivNth` #19467
- feat: `Clone` and some instances #20051
- feat: Definition of `Clone` #23460
- chore: fix recursors #23489
- Post's lattice #24744
- feat: a linter for duplicated `open` #25362
- chore: rename arguments of `Nat.strong_induction_on` #41540
7 open pull requests (0 with relevant labels)
Other
- feat(Algebra/Order/Field/Basic): generalize lemmas #24378
- feat(Tactic/Push): add basic tags and tests #29000
- refactor: use `OrderSupInfSet` #35263
- refactor: use `OrderSupSet` in `ConditionallyCompleteLattice` #35674
- refactor(Order/(Conditionally)CompletePartialOrder): extends `OrderSupSet` #38444
- test(Tactic/Algebra): try to replace `ring` with algebra in many places #38637
- chore(Data/Real): encapsulate real numbers #38702
12 open pull requests (0 with relevant labels)
Other
- 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
- chore: fix links #27709
- feat(Tactic/Push): add basic tags and tests #29000
- perf: remove some `aesop`s and `grind`s #35738
- feat(Topology/Compactness/CompactSystem): closed and compact square cylinders form a compact system #36160
- feat(Data/Set): add `Set.diag` #38380
- refactor: turn `Set` into a 1-field structure #39211
- feat: `Pi.map` rename to `Function.map` #39233
- refactor(Data): make `Set` a one-field structure #41506
- chore(Data/Set): move lemmas from `Set.Disjoint` to `Disjoint` #41913
- chore(Basic): move `FunLike` from Data #43253
5 open pull requests (0 with relevant labels)
Other
- refactor(Algebra/Group): make `IsUnit` a typeclass #17458
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- chore: rename arguments of `Nat.strong_induction_on` #41540
- feat(FieldTheory): extension is separable if its degree is less than the positive char #43205
- feat: `wlog` dischargers (`grind` by default) #43315
7 open pull requests (0 with relevant labels)
Other
- refactor(Algebra/Group): make `IsUnit` a typeclass #17458
- add subsingleton case to ExpChar #38154
- refactor(Algebra): semialgebra maps #38376
- chore(Algebra): consolidate variables and sections for `AlgHom`/`AlgEquiv` #38964
- chore: remove unused `haveI` and `letI` #41625
- chore(FieldTheory/IntermediateField/Adjoin): fix recursors #42856
- chore: deprecate monad operations on `MvPolynomial` #43372
1 open pull request (0 with relevant labels)
10 open pull requests (0 with relevant labels)
Other
- feat: more linting of cdots #12411
- test make `HasQuotient` out put a `setoid` #15586
- Clean up quotient APIs #16210
- chore(Data/Quot): deprecate `ind*'` APIs #16314
- chore: remove global `Quotient.mk` `⟦·⟧` notation #17127
- chore: dedent `to_additive` docstrings #28298
- feat: instance diamond linter #38781
- chore: replace terminal `convert` with `exact` #41762
- chore: prefer `beta_reduce` over `(d)simp only` #41933
- feat(GroupTheory/IndexNormal): the index of the normal core is bounded by the factorial of the index #43298
7 open pull requests (0 with relevant labels)
Other
- Clean up quotient APIs #16210
- 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
- feat(GroupTheory/SpecificGroups/Cyclic): comparison of subgroups of a cyclic group #40597
- feat(GroupTheory/Index): formula for index of centralizer of an element #41860
- feat(GroupTheory): virtually cyclic groups #43239
10 open pull requests (0 with relevant labels)
Other
- feat(AlgebraicGeometry/EllipticCurve/Scheme): define the affine scheme associated to an elliptic curve #25983
- feat(MonoidAlgebra): criteria for `single` to be a unit, irreducible or prime #27950
- feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories #30366
- feat(GroupTheory/SpecificGroups/Cyclic): a quotient of a cyclic group is cyclic #34186
- feat(GroupTheory/SpecificGroups/Cyclic): comparison of subgroups of a cyclic group #40597
- chore: rename arguments of `Nat.strong_induction_on` #41540
- chore: add missing `to_additive` docstrings #41628
- feat(GroupTheory): coatoms of the subgroup lattice #41651
- feat(GroupTheory/PGroup): maximal subgroups of abelian p-groups have index p #41652
- chore(GroupTheory/Archimedean): spell cyclic results using `IsCyclic` #43245
No open pull requests.
No open pull requests.
4 open pull requests (0 with relevant labels)
Other
- feat(NumberTheory/Modular): stabilizers for action on upper halfplane #33461
- chore: remove unused `haveI` and `letI` #41625
- feat(LinearAlgebra/Matrix/GeneralLinearGroup/Defs): add the proof of the range of toGL to be the ker of the determinant and the induced equivalence #41786
- feat(LinearAlgebra/Matrix/GeneralLinearGroup/Card): add the theorem on the cardinality of the special linear group over a commring and over a finite field #41979
4 open pull requests (0 with relevant labels)
Other
8 open pull requests (0 with relevant labels)
Other
- feat: move `ContinuousSMul` to a finite extension with the module topology #31948
- chore: prefer `Pi.single i 1 j` over `fun j => if i = j then 1 else 0` #31949
- feat: `Pi.map` rename to `Function.map` #39233
- feat(Algebra): use `Is*Apply` for `LinearMap` #39638
- feat: relate `Hom.piMap` and `Subobject.pi` #41686
- feat: generalize `MonoidHom.isStrictMap_prodMap` to arbitrary products #41693
- chore: replace terminal `convert` with `exact` #41762
- refactor(Data/SetLike): generalise `IsConcreteLE` #42666
No open pull requests.
No open pull requests.
No open pull requests.
No open pull requests.
No open pull requests.
No open pull requests.
No open pull requests.
5 open pull requests (0 with relevant labels)
Other
- chore: migrate to `tfae` block tactic #11003
- feat: check indentation of doc-strings #27897
- chore: fix markdown list indentation #35281
- chore: specify doc-strings of auto-generated additive declarations di… #41565
- chore(Order/WithBot): remove defeq between `WithBot.LE`/`LT` and `WithTop.LE`/`LT` #42622
No open pull requests.
6 open pull requests (0 with relevant labels)
Other
- chore: make `finiteness` a default tactic #26090
- feat(Tactic/Push): add basic tags and tests #29000
- feat(MeasureTheory): use `IsApply` for `Measure` #41177
- chore(MeasureTheory): using ENNReal instead of NNReal #42261
- chore: split too long file Measure.MeasureSpace #42943
- chore: deprecate Measure.MeasureSpace #42944
No open pull requests.
3 open pull requests (0 with relevant labels)
1 open pull request (0 with relevant labels)
3 open pull requests (0 with relevant labels)
Other
3 open pull requests (0 with relevant labels)
2 open pull requests (0 with relevant labels)
20 open pull requests (0 with relevant labels)
Other
- chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom #9564
- chore(FieldTheory/KummerExtension): move some lemmas earlier #9978
- feat: more linting of cdots #12411
- Clean up quotient APIs #16210
- chore(Data/Quot): deprecate `ind*'` APIs #16314
- chore(RingTheory/Ideal): make `RingHom.ker` take a `RingHom` instead of `RingHomClass` #25138
- feat(AlgebraicGeometry/EllipticCurve/Scheme): define the affine scheme associated to an elliptic curve #25983
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- feat(RingTheory/AdjoinRoot): add IsFractionRing for AdjoinRoot #35157
- feat(Algebra): add liftEquiv for groups, rings, algebras, and adjoin roots #36086
- feat(Algebra/Category): the category of local extensions over a fixed field #37940
- refactor(Algebra): semialgebra maps #38376
- chore(Algebra): `coe_ringHom` -> `coe_toRingHom` #38966
- feat(RingTheory/LocalRing): `adjoinRoot` and local rings #41064
- feat(RingTheory/AdjoinRoot): add AdjoinRoot.isFractionRing #41443
- chore: rename arguments of `Nat.strong_induction_on` #41540
- refactor(Algebra/Polynomial): make into an `abbrev` of `AddMonoidAlgebra` #41981
- feat: isomorphism of `AdjoinRoot (f.comp g)` #42069
- feat: generalize `Polynomial.irreducible_comp` #42344
- feat(FieldTheory/KummerExtension): criterion for `X ^ n - C a` to be irreducible for even `n` #42923
13 open pull requests (0 with relevant labels)
Other
- feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition #25991
- feat : `v.adicCompletionIntegers K` is compact when `K` is a number field #30579
- feat: the adele ring of a number field is locally compact #36404
- chore(Topology): `UniformSpace.Completion` renames for morphisms #38039
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- refactor: make adicCompletionIntegers a type #41490
- chore: make `adicCompletion` and `Completion` print nicer #41702
- perf: speed up kernel typechecking of some of mathlib's slowest declarations #41705
- refactor(Data/SetLike): generalise `IsConcreteLE` #42666
- feat(RingTheory/DedekindDomain/AdicValuation): adic valuations are trivial on subfields #42771
- refactor(Algebra/GroupWithZero): SubgroupWithZero, and rebase the valuation value group on it #43000
- chore: lake shake --add-public --keep-implied --keep-prefix --fix #43073
- feat: `LiesOver` valuations on `adicCompletion` #43427
6 open pull requests (0 with relevant labels)
Other
- chore: redefine `Ideal.IsPrime` #31595
- bench: review #39049
- feat(RingTheory/Ideal): generalize span_singleton_dvd_span_singleton_iff_dvd and emultiplicity_eq_emultiplicity_span #40557
- feat(NumberTheory/NumberField): summability of the prime ideal zeta sum #42567
- refactor(Data/SetLike): generalise `IsConcreteLE` #42666
- chore(RingTheory/Ideal/GoingUp): use `Ideal.under` #43414
5 open pull requests (0 with relevant labels)
Other
- chore(Data/Quot): deprecate `ind*'` APIs #16314
- 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
- refactor: make `IsAtom` not depend on `OrderBot` #40369
- chore: remove redudant haveI/letI in defs #41680
No open pull requests.
1 open pull request (0 with relevant labels)
5 open pull requests (0 with relevant labels)
Other
- refactor(Algebra/Module/LocalizedModule): Redefine `LocalizedModule` in terms of `OreLocalization`. #13156
- chore: get rid of `LocalizedModule.mk` #34248
- feat(RingTheory): algebra maps between finite étale algebras are locally finite split #38586
- chore(RingTheory): equality of linear map with values in finite module spreads out #38649
- chore: refactor Algebra.TensorProduct.rightAlgebra #39699
No open pull requests.
2 open pull requests (0 with relevant labels)
1 open pull request (0 with relevant labels)
1 open pull request (0 with relevant labels)
No open pull requests.
No open pull requests.
6 open pull requests (0 with relevant labels)
Other
- perf: reorder `extends` and change instance priority in algebra hierarchy #7873
- chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` #23621
- feat(AlgebraicGeometry/EllipticCurve/Scheme): define the affine scheme associated to an elliptic curve #25983
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore: remove `CovariantClass` and `ContravariantClass` #42273
- refactor(Data/SetLike): make second parameter of `*.ofSetLike` implicit #42705
9 open pull requests (0 with relevant labels)
Other
- feat(RingTheory): `ValuativeRel` on subrings #30135
- feat(RingTheory): valuative topology = adic topology for discrete rank 1 valuations #30192
- chore: redefine `Ideal.IsPrime` #31595
- feat(Valued/ValuationTopology): creating instances of `IsValuativeTopology` on completion #36769
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore(Order): infer `toDecidable*` in `*LinearOrder`s when possible #39908
- chore: replace `simp_all` with `simp` whenever possible #41896
- refactor(Algebra/GroupWithZero): SubgroupWithZero, and rebase the valuation value group on it #43000
- feat: `LiesOver` valuations on `adicCompletion` #43427
No open pull requests.
12 open pull requests (0 with relevant labels)
Other
- feat(Data/ZMod/Defs): Topological structure on `ZMod` #9146
- feat: rename `connectedComponentOfOne` to `identityComponent`, prove that it is normal and open #10024
- chore: fix some explicitVarOfIff linter errors #32095
- feat: prove strict group homs are stable under Prod.map #39270
- refactor(Topology/Algebra): use `IsOpenUnits` more widely #40379
- feat(Analysis): the inclusion of the general linear group into linear maps is an open embedding for finite-dimensional TVS #40380
- chore(Topology): rename `IndiscreteTopology` to `HasIndiscreteTopology` #40994
- feat(Topology/Algebra/Module): introduce the projective locally convex tensor product topology #42127
- feat: add a wrapper around `fun_prop` that calls `simp` on the function #42398
- feat(Order/Monoid/Unbundled): make `mulLeftMono_of_mulLeftStrictMono` and `mulRightMono_of_mulRightStrictMono` instances. #42456
- chore: remove declarations deprecated between 2021-08-11 and 2026-02-11 #42655
- chore: lake shake --add-public --keep-implied --keep-prefix --fix #43073
3 open pull requests (0 with relevant labels)
Other
2 open pull requests (0 with relevant labels)
No open pull requests.
6 open pull requests (0 with relevant labels)
Other
- refactor: deprecate `SemilinearMapClass` #18805
- refactor: deprecate `ContinuousLinearMapClass` #33448
- refactor: deprecate `LinearIsometryClass` #33450
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- feat(Topology): use `FComp` in `ContinuousLinearMap` #41224
- feat: introduce an IsNormableSpace class #42983
No open pull requests.
3 open pull requests (0 with relevant labels)
Other
5 open pull requests (0 with relevant labels)
Other
No open pull requests.
5 open pull requests (0 with relevant labels)
Other
- feat(Valued/ValuationTopology): creating instances of `IsValuativeTopology` on completion #36769
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- refactor(Algebra/GroupWithZero): SubgroupWithZero, and rebase the valuation value group on it #43000
- feat(ValuativeTopology): valuative topology of Z_p #43285
- feat: `LiesOver` valuations on `adicCompletion` #43427
7 open pull requests (0 with relevant labels)
Other
- chore: refactor algebraic filter bases #18202
- 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
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore: remove redudant haveI/letI in defs #41680
- refactor(Algebra/GroupWithZero): SubgroupWithZero, and rebase the valuation value group on it #43000
4 open pull requests (0 with relevant labels)
Other
2 open pull requests (0 with relevant labels)
No open pull requests.
2 open pull requests (0 with relevant labels)
No open pull requests.
No open pull requests.
Files easy to unlock
The following files do not depend on any other file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.