mathlib

9713e960 - chore(*): update to Lean 3.21.0c (#4578)

chore(*): update to Lean 3.21.0c (#4578) The only real change is the removal of notation for `vector.cons`. Co-authored-by: Johan Commelin <johan@commelin.net>