mathlib3
db84f2b6 - feat(data/polynomial): `aeval_alg_equiv`, like `aeval_alg_hom` (#8038)

Commit

4 years ago

feat(data/polynomial): `aeval_alg_equiv`, like `aeval_alg_hom` (#8038) This PR copies `polynomial.aeval_alg_hom` and `aeval_alg_hom_apply` to `aeval_alg_equiv(_apply)`.

Author

Vierkantor

Parents

2a155208

mathlib3 db84f2b6 - feat(data/polynomial): `aeval_alg_equiv`, like `aeval_alg_hom` (#8038)

mathlib3
db84f2b6 - feat(data/polynomial): `aeval_alg_equiv`, like `aeval_alg_hom` (#8038)