Commit 2024-01-29 05:23 4e0ccc00

View on Github →

feat(Data/Fin/Tuple/Basic): repeat_comp_rev (#9845) Prove repeat_comp_rev.

Estimated changes

added theorem Fin.modNat_rev
modified theorem Fin.size_positive
added theorem Fin.repeat_comp_rev
added theorem Fin.repeat_rev