mathlib

mathlib copied to clipboard

This PR adds `root_set_prod` (based on `roots_prod`) and cleans up lemma statements (the file already has `{R S : Type*} [field R]`). --- [](https://gitpod.io/from-referrer/)

tb65536

feat(field_theory/splitting_field): Adjoining all of the roots of a polynomial gives a splitting field

1

This PR proves that if `p` splits in a field extensions, then adjoining all of the roots of `p` gives a splitting field of `p`. --- - [x] depends on:...

tb65536

chore(computability/primrec): remove nolints

1

We add some documentation, and golf slightly by marking `nat.elim` and `nat.cases` as `reducible`. --- [](https://gitpod.io/from-referrer/)

vihdzp

iterated_deriv.lean was not used anywhere, and derivative.lean already had independent variants of several of the lemmas there, without the `iterated_deriv` indirecion. It seems better to consolidate these results. --- I...

Ruben-VandeVelde

feat(order/heyting/regular): Heyting-regular elements

1

Define Heyting-regular elements of an Heyting lattice, namely those `a` such that `aᶜᶜ = a`, and prove that they form a boolean algebra. --- - [ ] depends on: #15305...

YaelDillies

feat(catgory_theory/sites): Image sheaf

2

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

erdOne

feat(order/heyting_algebra): Heyting algebras

5

Define (generalized) Heyting, co-Heyting and bi-Heyting algebras. --- - [x] depends on: #15302 - [x] depends on: #15304 - [x] depends on: #15340 This a second go at #5527. I...

YaelDillies

introduce H-spaces and prove basic properties, in particular that every topological group is a H-space and that the path space at a point is a H-space. --- - depends on:...

faenuccio

Fix the linting errors coming from `fintype_finite`, `to_additive_doc` and `doc_blame`. --- [](https://gitpod.io/from-referrer/)

YaelDillies

feat(algebra/order/floor): The image of `floor`/`ceil` under an order ring hom

1

`⌊f a⌋ = ⌊a⌋`, `⌈f a⌉ = ⌈a⌉` and similar for `f` a strictly monotone ring homomorphism. --- - [ ] depends on: #16024 @eric-wieser, those are the lemmas I...

YaelDillies