Commit 2023-02-14 10:34 364f4696

View on Github →

feat: port Data.Finsupp.Lex (#2272)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/Lex.lean

added theorem Finsupp.lex_def

added theorem Finsupp.lex_eq_invImage_dfinsupp_lex

added theorem Finsupp.lex_lt_of_lt

added theorem Finsupp.lex_lt_of_lt_of_preorder

added theorem Finsupp.lt_of_forall_lt_of_lt

added theorem Finsupp.toLex_monotone

added theorem Pi.lex_eq_finsupp_lex