Revision #1380 → #1769 · back to history
addedDoubly stochastic matrix0ae7afd3bf5d
modifiedBirkhoff–von Neumann theorem12cf4959ac66
| Field | From #1380 | To #1769 |
|---|
| note | Mathlib proves the set of doubly stochastic matrices is the convex hull of permutation matrices, i.e. each is a convex combination of permutation matrices. | Mathlib proves the set of doubly stochastic matrices equals the convex hull of permutation matrices, i.e. each is a convex combination of permutation matrices. |
modifiedExistence for all orders except 2cba64012468b
| Field | From #1380 | To #1769 |
|---|
| anchor.snippet | Magic squares are believed to exist for all orders, except for order 2 | Magic squares exist for all orders except for order 2 |
| note | Existence of magic squares for all orders is not formalized in Mathlib. | Existence of magic squares for all orders except 2 is not formalized in Mathlib. Snippet corrected to match article text. |
| provenance | ai | ai-moderated |