basic): `add_submonoid.closure` of monomials is `⊤` (#11101)

Commit

4 years ago

feat(data/polynomial/basic): `add_submonoid.closure` of monomials is `⊤` (#11101) Use it to golf `polynomial.add_hom_ext`.

Author

urkud

Parents