Revision #2930 → #3422 · back to history
7130342c86a8| Field | From #2930 | To #3422 |
|---|---|---|
| note | No `median` of a finite list/multiset is defined anywhere in `Mathlib/`. | No statistical `median` of a finite list/multiset is defined in `Mathlib/` (the only `median` there is the geometric simplex median in `Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid`). |
9030978461c3d37fd5993a55