mathlib

mathlib copied to clipboard

Also provide `nonempty.coe_sort` and `nontrivial.coe_sort` aliases for dot notation. --- [](https://gitpod.io/from-referrer/)

YaelDillies

refactor(algebraic_geometry/projective_spectrum/topology): refactor projective_spectrum def into structure

1

- [x] depends on: #16920 [refactor height one spectrum] - [ ] depends on: #16930 [refactor prime spectrum] --- [](https://gitpod.io/from-referrer/)

Multramate

refactor(algebraic_geometry/prime_spectrum/basic): refactor prime_spectrum def into structure

1

- [x] depends on: #16920 [refactor height one spectrum] --- [](https://gitpod.io/from-referrer/)

Multramate

feat(algebraic_geometry/prime_spectrum/basic): intersection of localisations

5

- [x] depends on: #16905 [define maximal spectrum] - [x] depends on: #16920 [refactor height one spectrum] --- [](https://gitpod.io/from-referrer/)

Multramate

feat(topology/algebra/infinite_sum): generalize `tsum_le_of_sum_range_le`

2

--- Used by #16882 [](https://gitpod.io/from-referrer/)

kex-y

* From the sphere eversion project --- [](https://gitpod.io/from-referrer/)

fpvandoorn

feat(analysis/normed_space/basic): the left-regular representation is an isometry for (even non-unital) C⋆-algebras

1

This is a key tool to show that the multiplier algebra is a C⋆-algebra. - [ ] depends on: #16963 --- [](https://gitpod.io/from-referrer/)

j-loreaux

feat(analysis/convolution): prove associativity under more convenient assumptions

1

* Prove `convolution_assoc` which has as hypotheses things that are a lot more natural to check. The old version (that has a bit weaker assumptions) is renamed to `convolution_assoc'` *...

fpvandoorn

feat(geometry/euclidean/oriented_angle): refactor to a basis-free definition

1

Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/adding.20angles --- [](https://gitpod.io/from-referrer/) - [x] depends on: #16475 - [x] depends on: #16476 - [x] depends on: #16477 - [x] depends on: #16478 - [x] depends on:...

hrmacbeth

feat(analysis/inner_product_space/two_dim): the case of `ℂ`

1

This file relates the constructions `orientation.area_form`, `orientation.right_angle_rotation`, `orientation.kahler` on an oriented two-dimensional real inner product space to their concrete interpretations over `ℂ`. --- [](https://gitpod.io/from-referrer/) - [x] depends on:...

hrmacbeth