Commit 2024-05-16 18:36 e7c71eb1

View on Github →

chore: Reduce imports to Data.Finset.Image (#12832)

Estimated changes

Modified Mathlib/Algebra/Group/Nat.lean

Modified Mathlib/Data/Finset/Card.lean

modified theorem Finset.card_pos

Modified Mathlib/Data/Finset/Fold.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/Lattice.lean

Modified Mathlib/Data/Finset/Prod.lean

Modified Mathlib/Data/Nat/Interval.lean

Modified Mathlib/Data/Set/Enumerate.lean

Modified Mathlib/Order/SuccPred/LinearLocallyFinite.lean

modified theorem toZ_nonneg

Modified Mathlib/RingTheory/Prime.lean