mathlib

6309c816 - chore(ring_theory/adjoin) elab_as_eliminator attribute (#9168)