Commit 2023-01-23 07:56 f7baace5

View on Github →

feat: port Combinatorics.Hall.Finite (#1763)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Hall/Finite.lean

added theorem Finset.all_card_le_bunionᵢ_card_iff_existsInjective'

added theorem HallMarriageTheorem.hall_cond_of_compl

added theorem HallMarriageTheorem.hall_cond_of_erase

added theorem HallMarriageTheorem.hall_cond_of_restrict

added theorem HallMarriageTheorem.hall_hard_inductive

added theorem HallMarriageTheorem.hall_hard_inductive_step_A

added theorem HallMarriageTheorem.hall_hard_inductive_step_B