Commit 2024-07-31 06:44 1409ad6a

View on Github →

feat(Data/Matroid/Sum): Sums of matroids (#15061) This PR defines the sum of a pair or collection of matroids, and gives basic API. The material in Matroid/Map makes this both more general and shorter than #12380 , which got a bit snarled up in review.

depends on: #15060
depends on: #15057

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Matroid/Sum.lean

added theorem Matroid.Base.eq_union_image_of_disjointSum

added theorem Matroid.Finitary.sigma

added theorem Matroid.Finitary.sum'

added theorem Matroid.Indep.eq_union_image_of_disjointSum

added theorem Matroid.disjointSigma_base_iff

added theorem Matroid.disjointSigma_basis_iff

added theorem Matroid.disjointSigma_ground_eq

added theorem Matroid.disjointSigma_indep_iff

added def Matroid.disjointSum

added theorem Matroid.disjointSum_base_iff

added theorem Matroid.disjointSum_basis_iff

added theorem Matroid.disjointSum_ground_eq

added theorem Matroid.disjointSum_indep_iff

added theorem Matroid.sigma_base_iff

added theorem Matroid.sigma_basis_iff

added theorem Matroid.sigma_ground_eq

added theorem Matroid.sigma_indep_iff

added theorem Matroid.sum'_base_iff

added theorem Matroid.sum'_basis_iff

added theorem Matroid.sum'_ground_eq

added theorem Matroid.sum'_indep_iff

added theorem Matroid.sum_base_iff

added theorem Matroid.sum_basis_iff

added theorem Matroid.sum_ground

added theorem Matroid.sum_indep_iff