mathlib4

mathlib4 copied to clipboard

chore: Move Nat.instLinearOrder to Init.Order.Defs

10

It turns out that pushing the dependency out is quite annoying, so as an alternative, we propose considering Preorder, PartialOrder and LinearOrder to be foundational type classes that all of...

Ruben-VandeVelde

feat(AlgebraicGeometry/Morphisms): stalkwise constructor and more API

2

Adds a `MorphismProperty.stalkwise` constructor for morphism properties of schemes from a property of ring homomorphisms. Also adds API for reducing proofs of stability under base change to affine situations for...

chrisflav

refactor(CharP): make variables explicit + refactor

4

Follows up on Yael's comment in #8612 by making `n` (in `x ^ (p ^ n)`) explicit. --- - [ ] depends on: #8612 Lucas' Theorem CI should fail in...

grhkm21

feat(AlgebraicGeometry/Limits): Spec preserves finite coproducts

2

--- - [ ] depends on: #14429 [](https://gitpod.io/from-referrer/)

erdOne

feat: Unfold widget

2

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

PatrickMassot

refactor(AlgebraicGeometry): Rework `Morphisms/Basic` to phase away from TFAEs

1

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

erdOne

Feat: add `PowerBasis.exists_sModEq`

3

We add `PowerBasis.exists_sModEq`. From `flt-regular`. --- [](https://gitpod.io/from-referrer/)

riccardobrasca

dev: `#min_imps` command

1

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

adomani

refactor(Mathlib/Data/Seq/Seq): make `Seq'.mem_rec_on` more useful

3

```lean theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s) (h1 : ∀ b s', a = b ∨ C s' → C (cons...

Komyyy

feat(LocalExtr/LineDeriv): new file

1

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

urkud