Commit 2024-12-25 13:34 3fd2f541

View on Github →

chore(Data/Matroid): refactoring ext lemmas (#19664)

Estimated changes

Modified Mathlib/Data/Matroid/Basic.lean

deleted theorem Matroid.eq_iff_indep_iff_indep_forall

deleted theorem Matroid.eq_of_base_iff_base_forall

deleted theorem Matroid.eq_of_indep_iff_indep_forall

added theorem Matroid.ext_base

added theorem Matroid.ext_base_indep

added theorem Matroid.ext_iff_base

added theorem Matroid.ext_iff_indep

added theorem Matroid.ext_indep

modified structure Matroid

Modified Mathlib/Data/Matroid/Closure.lean

Modified Mathlib/Data/Matroid/Constructions.lean

Modified Mathlib/Data/Matroid/Dual.lean

Modified Mathlib/Data/Matroid/Map.lean

Modified Mathlib/Data/Matroid/Restrict.lean