Commit 2025-02-17 17:27 7aad3778

View on Github →

chore(Matroid/Restrict): fix omissions in #21879 (#21992) While updating my repo, I discovered a few mistakes I made in #21879 . This PR fixes them.

Estimated changes

Modified Mathlib/Data/Matroid/Basic.lean

deleted theorem Matroid.ExchangeProperty.encard_base_eq

added theorem Matroid.ExchangeProperty.encard_isBase_eq

Modified Mathlib/Data/Matroid/Closure.lean

deleted theorem Matroid.Indep.inter_IsBasis_biInter

deleted theorem Matroid.Indep.inter_IsBasis_iInter

deleted theorem Matroid.Indep.inter_IsBasis_sInter

added theorem Matroid.Indep.inter_isBasis_biInter

added theorem Matroid.Indep.inter_isBasis_iInter

added theorem Matroid.Indep.inter_isBasis_sInter

Modified Mathlib/Data/Matroid/IndepAxioms.lean

Modified Mathlib/Data/Matroid/Restrict.lean

deleted theorem Matroid.Base.isBasis_of_isRestriction

added theorem Matroid.IsBase.isBasis_of_isRestriction

deleted theorem Matroid.IsBasis.base_of_base_subset

added theorem Matroid.IsBasis.isBase_of_isBase_subset

deleted theorem Matroid.IsBasis.restrict_base

added theorem Matroid.IsBasis.restrict_isBase