Revision #1843 → #2352 · back to history
508c0eb149061b57c218abe6| Field | From #1843 | To #2352 |
|---|---|---|
| mathlib.decl | Snowflaking | Metric.Snowflaking |
| note | `Snowflaking` formalizes the power-of-d snowflake; the general concave-f version is not stated. | `Metric.Snowflaking X α` formalizes the power-of-d snowflake; the general concave-f version is not stated. |