mathlib
03775fbb - chore(data/mv_polynomial): aeval_rename -> aeval_id_rename (#4230)

Commit
5 years ago
chore(data/mv_polynomial): aeval_rename -> aeval_id_rename (#4230) `aeval_rename` was not general enough, so it is renamed to `aeval_id_rename`. Also: state and prove the more general version of `aeval_rename`.
Author
Parents
Loading