mathlib3

cdd05728 - chore(ring_theory/algebraic): fix typo + golf (#12834)