Commit 2025-08-22 21:50 4e662f3a

View on Github →

chore(Data/Finset): deprecate Finset.exists_ne_of_one_lt_card (duplicate) (#28437)

Estimated changes

Modified Mathlib/Algebra/Group/UniqueProds/Basic.lean

Modified Mathlib/Data/Finset/Card.lean

deleted theorem Finset.exists_ne_of_one_lt_card

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

Modified Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean