mathlib3

3d4f085e - chore(ring_theory/ideal): docstring for Krull's theorem and a special case (#3831)