Commit 2026-04-06 16:32 35186be3

View on Github →

feat(Data/Finsupp): add computational lemmas for cons and single (#35329) This PR introduces cons_injective2, cons_eq_single_zero_iff and cons_eq_single_succ_iff, which are helper lemmas designed to facilitate calculations (or simplification) of equalities involving Finsupp.cons and Finsupp.single.

Estimated changes

Modified Mathlib/Data/Finsupp/Fin.lean

added theorem Finsupp.cons_eq_single_succ_iff

added theorem Finsupp.cons_eq_single_zero_iff

added theorem Finsupp.cons_injective2

modified theorem Finsupp.cons_right_injective

added theorem Finsupp.cons_zero_eq_single_zero

added theorem Finsupp.cons_zero_single_eq_single_succ

modified theorem Finsupp.cons_zero_zero