mathlib4

mathlib4 copied to clipboard

https://leanprover-community.github.io/mathlib_docs/tactic/delta_instance.html#tactic.delta_instance_handler

gebner

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

adomani

feat(Data/Nat/Prime): add 2 theorems

2

--- We have 2 `exists_dvd_of_not_prime`, but not the other way round. I found these 2 theorems useful when proving a number is not a prime number. [](https://gitpod.io/from-referrer/)

casavaca

feat(Analysis/PSeries): add Schlömilch's generalization of the Cauchy condensation test

3

It is my first PR to mathlib4 so comments on how to improve on the formalisation are welcome. --- [](https://gitpod.io/from-referrer/)

deepimpactmir

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

hmonroe

Found by a WIP linter in #10235 --- [](https://gitpod.io/from-referrer/)

urkud

feat: Infinite products

1

Last year, YaelDillies made a pull request to mathlib3 that unfortunately never got merged in: https://github.com/leanprover-community/mathlib/pull/18405. This is the mathlib4 version of that pull request. We define arbitrarily indexed products...

trivial1711

feat: the root space of a Coxeter group and the bilinear form on it

11

Prepare to define the standard geometric representation of a Coxeter group by defining the root space and the bilinear form on it. Then prove some lemmas about the orthogonal reflections...

trivial1711

feat: reflections, inversion sequences in Coxeter groups

5

- Add theorem `List.length_eraseIdx_add_one` to `Data/List/Basic.lean`, which states that if `i < l.length`, then the length of `l.eraseIdx i plus one` is equal to the length of `l`. - Add...

trivial1711

feat: add length, reduced words in Coxeter groups

1

Add new file `GroupTheory/Coxeter/Length.lean`. Define the length function and reduced words of Coxeter groups. Prove their basic properties. I decided to split #11408 (now closed) into two pull requests. This...

trivial1711