Commit 2024-04-25 16:11 61ad21e8

View on Github →

feat(Data/Matroid/Dual): change dual notation (#12431) This PR changes the symbol for matroid duality from ﹡ to ✶. This is because there is a VSCode font rendering bug (discussed here) that causes ﹡ to display incorrectly when combined with certain other unicode symbols. Since the particular star ﹡ is only used for matroid duality in mathlib, this change is cosmetic and inconsequential.

Estimated changes

modified theorem Matroid.Base.ssubset_ground
modified theorem Matroid.Coindep.indep
modified theorem Matroid.Indep.coindep
modified theorem Matroid.coindep_def
modified theorem Matroid.dual_base_iff'
modified theorem Matroid.dual_base_iff
modified theorem Matroid.dual_coindep_iff
modified theorem Matroid.dual_dep_iff_forall
modified theorem Matroid.dual_dual
modified theorem Matroid.dual_ground
modified theorem Matroid.dual_inj
modified theorem Matroid.eq_dual_comm
modified theorem Matroid.eq_dual_iff_dual_eq
modified theorem Matroid.ground_not_base
modified theorem Matroid.setOf_dual_base_eq