Commit 2024-10-07 10:11 b18f6b58

View on Github →

feat(Data/Finsupp/Defs): induction_on_max (#16061) A finitely supported function can be built in ascending or descending order of "degree".

Estimated changes

Modified Mathlib/Data/Finsupp/Defs.lean

added theorem Finsupp.induction_on_max

added theorem Finsupp.induction_on_max₂

added theorem Finsupp.induction_on_min

added theorem Finsupp.induction_on_min₂