mathlib

f0eded9a - chore(algebra/ring/idempotents): golf iff_eq_zero_or_one (#13977)