mathlib3

716616b3 - chore(ring_theory/localization/basic): golf sec_snd_ne_zero (#15572)