Revision #3585 → #4110 · back to history
modifiedFour color theorem59c7173b5eff
| Field | From #3585 | To #4110 |
|---|
| note | Grep for `FourColor`/`four.color` returns no hits in Mathlib. | Loogle for `FourColor` returns zero hits in Mathlib. |
addedSymmetric polynomials16d6a853cdf2
modifiedTutte polynomial6b334f70ae3c
| Field | From #3585 | To #4110 |
|---|
| note | Grep for `Tutte.*polynomial`/`TuttePolynomial` returns no hits in Mathlib. | Loogle for `Tutte` returns only unrelated `destutter` hits; no Tutte polynomial in Mathlib. |
modifiedRamsey theory259ed965a5dc
| Field | From #3585 | To #4110 |
|---|
| note | The Hales–Jewett theorem (verified) — a Ramsey-type result — is formalized, but Ramsey's theorem itself is not stated directly. | The Hales–Jewett theorem (verified) — a Ramsey-type result — is formalized, but Ramsey's theorem itself is not stated directly (loogle for `Ramsey` returns zero hits). |
modifiedFinite Markov chainsfe933b7db9e7
| Field | From #3585 | To #4110 |
|---|
| mathlib.module | Mathlib.Probability.Kernel.Basic | Mathlib.Probability.Kernel.Defs |
| note | Mathlib has probability kernels (`ProbabilityTheory.Kernel`) and some Markov-chain infrastructure, but no dedicated finite-Markov-chain theory; `MeasureTheory.Kernel` (as originally cited) does not exist. | Mathlib has probability kernels (`ProbabilityTheory.Kernel`, verified in `Mathlib.Probability.Kernel.Defs`) and some Markov-chain infrastructure, but no dedicated finite-Markov-chain theory. |
modifiedMartin's axiom7afc111fb9a3
| Field | From #3585 | To #4110 |
|---|
| note | Grep finds no `MartinAxiom` declaration in Mathlib. | Loogle for `Martin` returns only Martingale-related decls; no `MartinAxiom` in Mathlib. |