aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/basic
diff options
context:
space:
mode:
authorKazuhiko Sakaguchi2020-11-10 22:01:19 +0900
committerKazuhiko Sakaguchi2020-11-11 00:46:20 +0900
commit88861b5dbd2803118222fe3a020317608c4c8500 (patch)
tree3e489204c714397fa5c1beaf6b323170554804c8 /mathcomp/basic
parentc312c678ac8af99d5c632285cbff5e1b55325478 (diff)
Remove `cycle_(mask|filter)` lemmas
Diffstat (limited to 'mathcomp/basic')
0 files changed, 0 insertions, 0 deletions