Skip to content

[Merged by Bors] - feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function #20921

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
apnelson1 wants to merge 13 commits into from
Closed

[Merged by Bors] - feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function #20921

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
c803cc9
initial
apnelson1 Jan 21, 2025
460a555
lint
apnelson1 Jan 21, 2025
d9d7008
typos
apnelson1 Jan 22, 2025
312f509
fix
apnelson1 Jan 22, 2025
9083478
Update Mathlib/Data/Matroid/Rank/Cardinal.lean
apnelson1 Jan 23, 2025
a314525
comments
apnelson1 Jan 23, 2025
4a30db2
docstring
apnelson1 Jan 23, 2025
02de685
remove typeclass assumptions
apnelson1 Jan 23, 2025
b95b475
fix
apnelson1 Jan 23, 2025
37b4115
fix
apnelson1 Jan 23, 2025
dfe549a
heterogeneity/naming
apnelson1 Jan 26, 2025
eb82f61
tidying
apnelson1 Jan 27, 2025
74c464f
comments
apnelson1 Jan 27, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions Mathlib/Data/Matroid/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -217,6 +217,9 @@ namespace Matroid

variable {α : Type*} {M : Matroid α}

instance (M : Matroid α) : Nonempty {B // M.Base B} :=
nonempty_subtype.2 M.exists_base

/-- Typeclass for a matroid having finite ground set. Just a wrapper for `M.E.Finite`-/
@[mk_iff] protected class Finite (M : Matroid α) : Prop where
/-- The ground set is finite -/
Expand Down
Loading