Commit 2025-08-07 15:29 32e40df2

View on Github →

chore(Finsupp): move order properties under Order (#25002)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/Order/Floor/Div.lean

Modified Mathlib/Data/Finsupp/Multiset.lean

Modified Mathlib/Data/Finsupp/Order.lean

deleted theorem Finsupp.coe_le_coe

deleted theorem Finsupp.coe_lt_coe

deleted theorem Finsupp.coe_mono

deleted theorem Finsupp.coe_strictMono

deleted theorem Finsupp.inf_apply

deleted theorem Finsupp.le_def

deleted theorem Finsupp.lt_def

deleted def Finsupp.orderEmbeddingToFun

deleted theorem Finsupp.orderEmbeddingToFun_apply

deleted theorem Finsupp.sup_apply

deleted theorem Finsupp.support_inf_union_support_sup

deleted theorem Finsupp.support_sup_union_support_inf

Modified Mathlib/Data/Finsupp/PWO.lean

Modified Mathlib/Data/Finsupp/Weight.lean

Modified Mathlib/Data/Nat/Choose/Multinomial.lean

Modified Mathlib/Data/Nat/Factorization/Defs.lean

Created Mathlib/Order/Preorder/Finsupp.lean

added theorem Finsupp.coe_le_coe

added theorem Finsupp.coe_lt_coe

added theorem Finsupp.coe_mono

added theorem Finsupp.coe_strictMono

added theorem Finsupp.inf_apply

added theorem Finsupp.le_def

added theorem Finsupp.lt_def

added def Finsupp.orderEmbeddingToFun

added theorem Finsupp.sup_apply

added theorem Finsupp.support_inf_union_support_sup

added theorem Finsupp.support_sup_union_support_inf