Revision #1014 → #2795 · back to history
0a834851ff9a| Field | From #1014 | To #2795 |
|---|---|---|
| note | The Koch curve is not defined in Mathlib. | The Koch curve is not defined in Mathlib (only the general Metric.Snowflaking construction is present, mentioning Koch in a docstring). |
4abae46eabdca9d8d8dece14