Commit 2025-04-10 16:17 ddb4ebec

View on Github →

feat(Matroid): loopless matroids (#23884) We define and give API for a Loopless typeclass for matroids and a removeLoops operation that deletes the loops of a matroid M.

Estimated changes

Modified Mathlib/Data/Matroid/Loop.lean

added theorem Matroid.IsNonloop.removeLoops_isNonloop

added theorem Matroid.IsRestriction.isRestriction_removeLoops

added theorem Matroid.IsRestriction.loopless

added theorem Matroid.Loopless.ground_eq

added theorem Matroid.compl_loops_eq

added theorem Matroid.eq_loopyOn_iff_loops

added theorem Matroid.eq_restrict_removeLoops

added theorem Matroid.isNonloop_of_loopless

added theorem Matroid.loopless_iff_forall_isCircuit

added theorem Matroid.loopless_iff_forall_isNonloop

added theorem Matroid.loopless_iff_forall_not_isLoop

added theorem Matroid.loops_eq_empty

added theorem Matroid.loopyOn_isLoopless_iff

added theorem Matroid.not_isLoop

added def Matroid.removeLoops

added theorem Matroid.removeLoops_eq_restrict

added theorem Matroid.removeLoops_eq_self

added theorem Matroid.removeLoops_eq_self_iff

added theorem Matroid.removeLoops_ground_eq

added theorem Matroid.removeLoops_idem

added theorem Matroid.removeLoops_indep_eq

added theorem Matroid.removeLoops_isBase_eq

added theorem Matroid.removeLoops_isBasis'_eq

added theorem Matroid.removeLoops_isNonloop_eq

added theorem Matroid.removeLoops_isRestriction

added theorem Matroid.removeLoops_mono_isRestriction

added theorem Matroid.removeLoops_restrict_eq_restrict

added theorem Matroid.restrict_subset_loops_eq

added theorem Matroid.restrict_univ_removeLoops_eq

added theorem Matroid.subsingleton_indep

Modified Mathlib/Data/Matroid/Minor/Basic.lean

added theorem Matroid.delete_loops_eq_removeLoops