mathlib3

863a1676 - docs(ring_theory/localization/ideal): fix an unused name (#13992)