div): prove that evaluation induces an isomorphism of algebras (#18480)

Commit

2 years ago

feat(data/polynomial/div): prove that evaluation induces an isomorphism of algebras (#18480) Also prove that `aeval` coerces to `eval_ring_hom`.

References

Author

Multramate

Parents