Commit 2024-12-04 18:37 0257491f

View on Github →

feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order (#19455) Definition of the homogeneous lexicographic order This is part of an ongoing work on basic of Gröbner theory. A subsequent PR will add the homogeneous reverse lexicographic order.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finsupp/Lex.lean

added theorem Finsupp.Lex.single_antitone

added theorem Finsupp.Lex.single_le_iff

added theorem Finsupp.Lex.single_lt_iff

added theorem Finsupp.Lex.single_strictAnti

Created Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

added theorem DegLex.exists_iff

added theorem DegLex.forall_iff

added def DegLex

added theorem Finsupp.DegLex.le_iff

added theorem Finsupp.DegLex.lt_def

added theorem Finsupp.DegLex.lt_iff

added theorem Finsupp.DegLex.monotone_degree

added theorem Finsupp.DegLex.single_antitone

added theorem Finsupp.DegLex.single_le_iff

added theorem Finsupp.DegLex.single_lt_iff

added theorem Finsupp.DegLex.single_strictAnti

added theorem Finsupp.DegLex.wellFounded

added theorem Finsupp.degLex_def

added theorem MonomialOrder.degLex_le_iff

added theorem MonomialOrder.degLex_lt_iff

added theorem MonomialOrder.degLex_single_le_iff

added theorem MonomialOrder.degLex_single_lt_iff

added def ofDegLex

added theorem ofDegLex_add

added theorem ofDegLex_inj

added theorem ofDegLex_injective

added theorem ofDegLex_symm_eq

added theorem ofDegLex_toDegLex

added def toDegLex

added theorem toDegLex_add

added theorem toDegLex_inj

added theorem toDegLex_injective

added theorem toDegLex_ofDegLex

added theorem toDegLex_symm_eq

Modified Mathlib/Data/Finsupp/Weight.lean

added theorem Finsupp.degree_add

added theorem Finsupp.degree_single