Commit 2025-05-17 04:25 6997e032

View on Github →

chore: improve simp set to prepare for improved simpNF linter (#24961)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finsupp/Basic.lean

added theorem Finsupp.prod_attach_index

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Finset/CastCard.lean

Modified Mathlib/Data/List/Basic.lean

modified theorem List.length_erase_add_one

Modified Mathlib/Data/Multiset/AddSub.lean

Modified Mathlib/Data/Multiset/FinsetOps.lean

added theorem Multiset.Nodup.inter

Modified Mathlib/Data/Set/Card.lean

modified theorem Set.ncard_diff_singleton_add_one

modified theorem Set.ncard_diff_singleton_of_mem

modified theorem Set.ncard_pair

Modified Mathlib/Dynamics/PeriodicPts/Defs.lean

added theorem Function.exists_iterate_apply_eq_of_mem_periodicPts

modified theorem Function.self_mem_periodicOrbit

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean