mathlib3
d31b85f8 - feat(data/list/rotate): is_rotated_append (#8780)

Commit
4 years ago
feat(data/list/rotate): is_rotated_append (#8780) `list.append` is commutative with respect to `~r`.
Author
Parents
Loading