mathlib4

mathlib4 copied to clipboard

chore (Algebra.Order.Nonneg.Ring): split into unbundled and bundled ordered algebra files

4

We split `Algebra.Order.Nonneg.Ring` into `Algebra.Order.Nonneg.Ring` which uses unbundled ordered algebra typeclasses, eg `CovariantClass`, and `Algebra.Order.Nonneg.OrderedRing` which uses bundled class, eg `OrderedAddComm`. Using this we can avoid importing bundled ordered algebra...

mattrobball

feat:(Condensed): properties of the functor from `TopCat` to `CondensedSet`

1

--- [](https://gitpod.io/from-referrer/)

dagurtomas

chore: Split `RingTheory.Trace` and `RingTheory.Norm`

1

We split `RingTheory.Trace` in `RingTheory.Trace.Defs` and `RingTheory.Trace.Basic`. Similarly for `RingTheory.Norm`. --- [](https://gitpod.io/from-referrer/)

riccardobrasca

feat(RingTheory/Congruence): interpret `RingCon` as two sided ideals

8

In this PR, we set up an instance `SetLike (RingCon R) R` for any `NonUnitalNonAssocRing R`. This enables us to interpret `RingCon R` as two-sided-ideals. Co-authored-by: Eric Wieser --- -...

jjaassoonn

chore (Algebra.Order.Field.Defs): split off results about unbundled ordered algebra

4

We should be able to use these results about unbundled ordered algebra without importing the heavy machinery of the bundled typeclasses. --- - [ ] depends on: #14393 [![Open in...

mattrobball

feat: API for multiequalizers in the category of types

1

In this PR, we give a concrete characterization of limit multiforks in the category of types. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in...

joelriou

feat(PowerSeries): coefficients of series products

1

Add three elementary lemmas about coefficients of series products. --- [](https://gitpod.io/from-referrer/)

rwst

feat: Group scheme structure on Weierstrass curve

1

--- [](https://gitpod.io/from-referrer/)

alreadydone

chore: Golf `Finset.exists_subsuperset_card_eq`

1

Thanks Bhavik! --- [](https://gitpod.io/from-referrer/)

YaelDillies

Feat (RingTheory/Ideal/KrullDimension): defined the Krull dimension of a ring.

5

The ring theoretic krull dimension is the order theoretic krull dimension applied to its prime spectrum. Unfolding this definition, it is the length of longest series of prime ideals ordered...

FMLJohn