feat(data/polynomial/ring_division): comp_eq_zero_iff (#6147)
feat(data/polynomial/ring_division): comp_eq_zero_iff (#6147)

Condition for a composition of polynomials to be zero (assuming that the ring is an integral domain).





leanprover-community/mathlib,leanprover-community/mathlib