Commit 2025-03-24 15:26 eb9e107a

feat(Data/Matroid/Loop): nonloops (#23157) We give a definition of nonloops of a matroid M with basic API, defined as elements of M.E that are not loops. We also change Matroid.loops from an abbrev to a def, since it causes the simpNF linter to complain about natural-looking lemma statements.