Commit 2024-07-29 07:19 bc33405d

View on Github →

feat(Data/Matroid/Map): add missing lemmas (#15060) We add a few missing lemmas, mostly about Matroid.Basis, in Matroid/Map, and also fix a couple of typos in the same file.

Estimated changes

Modified Mathlib/Data/Matroid/Map.lean

added theorem Matroid.mapEmbedding_base_iff

added theorem Matroid.mapEmbedding_basis_iff

added theorem Matroid.mapEquiv_basis_iff

added theorem Matroid.restrictSubtype_base_iff

added theorem Matroid.restrictSubtype_basis_iff

added theorem Matroid.restrictSubtype_ground_base_iff

added theorem Matroid.restrictSubtype_ground_basis_iff