mathlib

9f955fe5 - feat(ring_theory/integral_closure): Cleanup interface for ring_hom.is_integral (#5144)