mathlib4

mathlib4 copied to clipboard

feat(Algebra): additive `n`-torsion subgroups

1

For an `AddCommGroup` `A` and a natural number `n`, - Define `AddSubgroup.torsionBy A n` using `Submodule.torsionBy`. - Define a scoped notation `A[n]` - Equip `AddSubgroup.torsionBy A n` with a `ZMod...

wupr

Complete homogeneous and monomial symmetric polynomials

8

Implemented complete homogeneous symmetric functions. Request for comments. See also #10983. Co-authored-by: Nirvana Coppola [[email protected]](mailto:[email protected]) --- [](https://gitpod.io/from-referrer/)

SashaIr

refactor: golf proof using lmarginal

1

Co-authored-by: Heather Macbeth [[email protected]](mailto:[email protected]) --- [](https://gitpod.io/from-referrer/)

fpvandoorn

This is a new branch for handling the eigenvectorUnitary declaration and subsequent changes. --- [](https://gitpod.io/from-referrer/)

JonBannon

Characterise when `trailingDegree p = 0` and `natTrailingDegree p = 0`. Also fix a few names. --- [](https://gitpod.io/from-referrer/)

YaelDillies

Define spectral spaces and prove that a quasi-compact open of a spectral space is spectral. --- [](https://gitpod.io/from-referrer/)

pangelinos

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

wupr

Move `Finset.biUnion` and `Finset.disjiUnion` to a new file so that `Data.Finset.Basic` doesn't depend on that much order theory. --- [](https://gitpod.io/from-referrer/)

YaelDillies

This is the same as my DiscrTree PR in Std, but I've decided to move it over to Mathlib now. Additionally, I have added the `rw??` tactic which uses this...

JovanGerb

chore(Algebra.Ring.InjSurj): remove redundant `mul` and `add` fields

1

Lean can figure these out and if inferred instance of `Mul` (or `Add`) contains non-reducible terms, it will block unification. --- - [ ] depends on: #11521 [](https://gitpod.io/from-referrer/)

mattrobball