mathlib
964f0e53 - feat(data/polynomial): work over noncommutative rings where possible (#3193)

Commit
5 years ago
feat(data/polynomial): work over noncommutative rings where possible (#3193) After downgrading `C` from an algebra homomorphism to a ring homomorphism in [69931ac](https://github.com/leanprover-community/mathlib/commit/69931acfe7b6a29f988bcf7094e090767b34fb85), which requires a few tweaks, everything else is straightforward. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Alex J. Best <alex.j.best@gmail.com>
Author
Parents
Loading