Commit 2023-03-19 06:25 4d97a152

View on Github →

feat: port Data.Finsupp.WellFounded (#2985)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/WellFounded.lean

added theorem Finsupp.Lex.acc

added theorem Finsupp.Lex.wellFounded'

added theorem Finsupp.Lex.wellFounded

added theorem Finsupp.Lex.wellFoundedLT_of_finite

added theorem Finsupp.Lex.wellFounded_of_finite