Revision #1090 → #2026 · back to history
addedPascal's triangle / arithmetical triangleb30dc1ab24a7
addedHamiltonian cycles in Cayley graphs50894132cc34
addedFour color theorem59c7173b5eff
addedFibonacci numbers4ad42c38832e
addedTutte polynomial6b334f70ae3c
modifiedFinite geometrye67bea3c51a7
| Field | From #1090 | To #2026 |
|---|
| mathlib.decl | Configuration | Configuration.Nondegenerate |
| note | `Mathlib/Combinatorics/Configuration.lean` covers projective-plane-style finite incidence configurations, but the field is not defined as such. | `Mathlib/Combinatorics/Configuration.lean` covers projective-plane-style finite incidence configurations via `Configuration.Nondegenerate`, but the field is not defined as such. |
modifiedOrder theoryc0ea7396a36e
| Field | From #1090 | To #2026 |
|---|
| mathlib.module | Mathlib.Order.Defs | Mathlib.Order.Defs.PartialOrder |
addedLattices358dd41de240
addedBoolean algebras1c4d72de2a6f
addedPigeonhole principle84d417591f1c
modifiedAdditive number theoryd7d8ed7ee9b9
| Field | From #1090 | To #2026 |
|---|
| mathlib.decl | Finset.CauchyDavenport | ZMod.cauchy_davenport |
| note | Many additive number theory results are in `Mathlib/Combinatorics/Additive/`, but the subfield itself has no formal definition. | Many additive number theory results are in `Mathlib/Combinatorics/Additive/` (e.g. `ZMod.cauchy_davenport`), but the subfield itself has no formal definition. |
addedMartin's axiom7afc111fb9a3
addedPotts model and chromatic/Tutte polynomials181e46d2e8bd