Commit 2024-09-15 09:18 036e9566

View on Github →

chore(*): fix Decidable, Fintype/Finite (#16807)

Estimated changes

Modified Mathlib/Algebra/Group/AddChar.lean

modified theorem AddChar.sum_eq_ite

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

modified theorem SimpleGraph.ConnectedComponent.odd_card_supp_iff_odd_subcomponents

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

modified theorem SimpleGraph.ConnectedComponent.even_card_of_isPerfectMatching

modified theorem SimpleGraph.ConnectedComponent.odd_matches_node_outside

modified theorem SimpleGraph.exists_maximal_isMatchingFree

Modified Mathlib/Data/Matrix/Rank.lean

modified theorem Matrix.rank_add_rank_le_card_of_mul_eq_zero

Modified Mathlib/NumberTheory/JacobiSum/Basic.lean