basic): `polynomial.ker_map_ring_hom` and `mv_polynomial.ker_map` (#10160)

Commit

4 years ago

feat(ring_theory/polynomial/basic): `polynomial.ker_map_ring_hom` and `mv_polynomial.ker_map` (#10160)

Author

eric-wieser

Parents