Thomas Browning

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/)

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:...

feat(Topology/Algebra/PontryaginDual): Local Compactness of the Pontryagin Dual

2

This PR uses Arzela-Ascoli to prove local compactness of the Pontryagin dual. --- - [x] depends on: #11334 - [x] depends on: #6844 - [x] depends on: #12002 [![Open in...

WIP: Frobenius Elements

2

This PR proves the existence of Frobenius elements in algebraic number theory. --- - [ ] depends on: #17752 - [ ] depends on: #17753 - [x] depends on: #17849...

refactor(RingTheory/Ideal/Pointwise): Make `Ideal.IsPrime.smul` into an instance

1

This PR makes `Ideal.IsPrime.smul` into an instance (like how `Ideal.IsPrime.comap` is an instance). --- [](https://gitpod.io/from-referrer/)

feat(Data/Set/Card): criterion for `s.ncard ≤ (f '' s).ncard + 1`

1

This PR gives a criterion `s.ncard ≤ (f '' s).ncard + 1` (note that we always have the inequality `(f '' s).ncard ≤ s.ncard`). --- [](https://gitpod.io/from-referrer/)

feat: haar measures on short exact sequences

3

This PR defines the notion of a short exact sequence of topological groups, and proves that if `1 → A → B → C → 1` is a short exact...