mathlib
755cb75f - feat(data/list/basic): non-meta to_chunks (#7517)

Commit
4 years ago
feat(data/list/basic): non-meta to_chunks (#7517) A non-meta definition of the `list.to_chunks` method, plus some basic theorems about it.
Author
Parents
Loading