Commit 2024-08-01 19:15 cde75903

View on Github →

chore: three more Fintype -> Finite replacements (#15283) Found by the linter in #10235.

Estimated changes

Modified Mathlib/Data/Finset/Density.lean

modified theorem Finset.dens_filter_add_dens_filter_not_eq_dens

Modified Mathlib/Data/Fintype/CardEmbedding.lean

modified theorem Fintype.card_embedding_eq_of_infinite

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean