Commit 2025-01-29 23:20 34763b00

View on Github →

chore(Order/SupIndep): review API (#21235)

Estimated changes

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

Modified Mathlib/Order/SupIndep.lean

added theorem Finset.SupIndep.antitone_fun

deleted theorem Finset.SupIndep.attach

deleted theorem Finset.SupIndep.biUnion

deleted theorem Finset.SupIndep.image

deleted theorem Finset.SupIndep.product

deleted theorem Finset.SupIndep.sigma

deleted theorem Finset.SupIndep.sup

deleted theorem Finset.supIndep_antimono_fun