Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-05 11:05 225d1ce3

View on Github →

refactor(combinatorics/hall/finite): small simplifications and readability improvements (#13091)

Estimated changes

Modified src/combinatorics/hall/finite.lean

modified theorem hall_marriage_theorem.hall_hard_inductive

deleted theorem hall_marriage_theorem.hall_hard_inductive_step

deleted theorem hall_marriage_theorem.hall_hard_inductive_zero