mathlib3

974d23c2 - feat(data/polynomial/monic): add monic_of_mul_monic_left/right (#12446)

feat(data/polynomial/monic): add monic_of_mul_monic_left/right (#12446) Also clean up variables that are defined in the section. From https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60geom_sum.20.28X.20.20n.29.60.20is.20monic/near/274130839