Commit 2023-12-13 00:15 ef12d9df

View on Github →

feat: matroid duality (#8732) This PR adds the definition of the dual of a matroid and co-independent sets, as well as some notation and API.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Matroid/Basic.lean

Created Mathlib/Data/Matroid/Dual.lean

added theorem Matroid.Base.compl_base_dual

added theorem Matroid.Base.compl_base_of_dual

added theorem Matroid.Base.compl_inter_basis_of_inter_basis

added theorem Matroid.Base.inter_basis_iff_compl_inter_basis_dual

added theorem Matroid.Base.ssubset_ground

added theorem Matroid.Coindep.exists_base_subset_compl

added theorem Matroid.Coindep.exists_subset_compl_base

added theorem Matroid.Coindep.indep

added theorem Matroid.Coindep.subset_ground

added theorem Matroid.Indep.coindep

added theorem Matroid.Indep.ssubset_ground

added theorem Matroid.base_iff_dual_base_compl

added theorem Matroid.coindep_def

added theorem Matroid.coindep_iff_exists'

added theorem Matroid.coindep_iff_exists

added theorem Matroid.coindep_iff_subset_compl_base

added def Matroid.dual

added def Matroid.dualIndepMatroid

added theorem Matroid.dual_base_iff'

added theorem Matroid.dual_base_iff

added theorem Matroid.dual_coindep_iff

added theorem Matroid.dual_dep_iff_forall

added theorem Matroid.dual_dual

added theorem Matroid.dual_ground

added theorem Matroid.dual_indep_iff_exists'

added theorem Matroid.dual_indep_iff_exists

added theorem Matroid.dual_inj

added theorem Matroid.dual_injective

added theorem Matroid.dual_involutive

added theorem Matroid.eq_dual_comm

added theorem Matroid.eq_dual_iff_dual_eq

added theorem Matroid.ground_not_base

added theorem Matroid.setOf_dual_base_eq

Modified Mathlib/Data/Matroid/IndepAxioms.lean