Commit 2025-04-27 13:12 a801654a

View on Github →

chore(*): fix some Decidable*/Fintype assumptions (#24400) Cherry-picked from #10235

Estimated changes

Modified Mathlib/Algebra/Module/ZLattice/Covolume.lean

modified theorem ZLattice.covolume_eq_det_inv

modified theorem ZLattice.volume_image_eq_volume_div_covolume

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

modified theorem SimpleGraph.IsClique.card_le_cliqueNum

modified theorem SimpleGraph.exists_isNClique_cliqueNum

modified theorem SimpleGraph.exists_isNIndepSet_indepNum

modified theorem SimpleGraph.isIndepSet_neighborSet_of_triangleFree

Modified Mathlib/Data/DFinsupp/Defs.lean

Modified Mathlib/Data/Matrix/Bilinear.lean