Commit 2023-01-28 07:25 2c6b1aca

View on Github →

feat: Port/Data.Finsupp.Fin (#1895) Port of data.finsupp.fin

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/Fin.lean

added def Finsupp.cons

added theorem Finsupp.cons_ne_zero_iff

added theorem Finsupp.cons_ne_zero_of_left

added theorem Finsupp.cons_ne_zero_of_right

added theorem Finsupp.cons_succ

added theorem Finsupp.cons_tail

added theorem Finsupp.cons_zero

added theorem Finsupp.cons_zero_zero

added def Finsupp.tail

added theorem Finsupp.tail_apply

added theorem Finsupp.tail_cons