Commit 2025-02-24 09:31 1074b2c7

View on Github →

feat(Data/Matroid/Loop): matroid loops (#22045) We add a definition of a loop element of a matroid, with basic API.

Estimated changes

added theorem Matroid.IsLoop.closure
added def Matroid.IsLoop
added theorem Matroid.closure_empty
added theorem Matroid.comap_loops
added theorem Matroid.isLoop_iff
added theorem Matroid.isLoop_tfae
added theorem Matroid.map_isLoop_iff
added theorem Matroid.map_loops
added theorem Matroid.singleton_dep