Commit 2025-11-28 17:46 69064101

View on Github →

chore: remove a few unused Fintype assumptions in statements (#32151)

Estimated changes

Modified Mathlib/Combinatorics/SetFamily/FourFunctions.lean

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

Modified Mathlib/LinearAlgebra/Pi.lean

Modified Mathlib/Topology/DiscreteSubset.lean

added theorem discreteTopology_iUnion_finite

deleted theorem discreteTopology_iUnion_fintype