mathlib

e1fea3a1 - feat(ring_theory/ideal): the product and infimum of principal ideals (#9852)

feat(ring_theory/ideal): the product and infimum of principal ideals (#9852) Three useful lemmas for applying the Chinese remainder theorem when an ideal is generated by one, non-prime, element.