Order

📁 Source: Mathlib/Data/Finsupp/Order.lean

Statistics

Metric	Count
Definitions decidableLE, decidableLT, orderBot, tsub	4
Theorems addLeftReflectLE, add_eq_zero_iff, add_sub_single_one, bot_eq_zero, coe_tsub, disjoint_iff, instCanonicallyOrderedAddOfAddLeftMono, instPosSMulMono, instPosSMulReflectLE, instPosSMulStrictMono, instSMulPosMono, instSMulPosReflectLE, instSMulPosReflectLT, instSMulPosStrictMono, isOrderedAddMonoid, isOrderedCancelAddMonoid, le_iff, le_iff', mapDomain_mono, mapDomain_nonneg, mapDomain_nonpos, orderedSub, single_le_iff, single_le_single, single_mono, single_nonneg, single_nonpos, single_tsub, sub_add_single_one_cancel, sub_single_one_add, subset_support_tsub, sum_le_sum, sum_le_sum_index, sum_nonneg, sum_nonneg', sum_nonpos, sum_pos, sum_pos', support_inf, support_mono, support_monotone, support_sup, support_tsub, tsub_apply	44
Total	48

Finsupp

Definitions

Name	Category	Theorems
decidableLE 📖	CompOp	6 math math: MvPowerSeries.coeff_mul_monomial, MvPowerSeries.coeff_monomial_mul, MvPolynomial.coeff_monomial_mul', MvPowerSeries.coeff_trunc', MvPowerSeries.coeff_truncFun', MvPolynomial.coeff_mul_monomial'
decidableLT 📖	CompOp	5 math math: MvPowerSeries.coeff_inv, MvPowerSeries.coeff_inv_aux, MvPowerSeries.coeff_trunc, MvPowerSeries.coeff_truncFun, MvPowerSeries.coeff_invOfUnit
orderBot 📖	CompOp	4 math math: bot_eq_zero, disjoint_iff, card_Iic, card_Iio
tsub 📖	CompOp	27 math math: MonomialOrder.sPolynomial_leadingTerm_mul', MvPowerSeries.coeff_mul_monomial, MvPolynomial.coeff_X_mul', MvPowerSeries.coeff_monomial_mul, add_sub_single_one, sub_add_single_one_cancel, MvPolynomial.mkDerivationₗ_monomial, Nat.dvd_iff_div_factorization_eq_tsub, MonomialOrder.sPolynomial_def, MvPolynomial.coeff_monomial_mul', MvPolynomial.mkDerivation_monomial, single_tsub, MvPolynomial.coeff_mul_X', MonomialOrder.sPolynomial_monomial_mul, MvPolynomial.pderiv_monomial, subset_support_tsub, Nat.factorization_div, MonomialOrder.sPolynomial_monomial_mul', tsub_apply, weight_sub_single_add, coe_tsub, orderedSub, MvPolynomial.coeff_mul_monomial', sub_single_one_add, support_tsub, MonomialOrder.sPolynomial_mul_monomial, MonomialOrder.sPolynomial_leadingTerm_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addLeftReflectLE 📖	mathematical	—	AddLeftReflectLE Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAdd instLE Preorder.toLE PartialOrder.toPreorder	—	le_of_add_le_add_left
add_eq_zero_iff 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAdd instZero	—	Unique.instSubsingleton
add_sub_single_one 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid tsub Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Nat.instOrderedSub single	—	Nat.instCanonicallyOrderedAdd Nat.instOrderedSub add_tsub_assoc_of_le CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAddOfAddLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid isOrderedAddMonoid orderedSub addLeftReflectLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le single_le_iff
bot_eq_zero 📖	mathematical	—	Bot.bot Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid OrderBot.toBot instLE Preorder.toLE PartialOrder.toPreorder orderBot instZero	—	—
coe_tsub 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike tsub Pi.instSub	—	—
disjoint_iff 📖	mathematical	—	Disjoint Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid partialorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder orderBot Finset Finset.partialOrder Finset.instOrderBot support	—	disjoint_iff bot_eq_zero support_eq_empty support_inf
instCanonicallyOrderedAddOfAddLeftMono 📖	mathematical	—	CanonicallyOrderedAdd Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAdd instLE Preorder.toLE PartialOrder.toPreorder	—	ext add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE le_add_self le_self_add
instPosSMulMono 📖	mathematical	—	PosSMulMono Finsupp SMulZeroClass.toSMul instZero smulZeroClass preorder	—	PosSMulMono.lift Pi.instPosSMulMono coe_le_coe coe_smul
instPosSMulReflectLE 📖	mathematical	—	PosSMulReflectLE Finsupp SMulZeroClass.toSMul instZero smulZeroClass preorder	—	PosSMulReflectLE.lift Pi.instPosSMulReflectLE coe_le_coe coe_smul
instPosSMulStrictMono 📖	mathematical	—	PosSMulStrictMono Finsupp SMulZeroClass.toSMul instZero smulZeroClass SMulWithZero.toSMulZeroClass PartialOrder.toPreorder preorder	—	PosSMulStrictMono.lift Pi.instPosSMulStrictMono coe_le_coe coe_smul
instSMulPosMono 📖	mathematical	—	SMulPosMono Finsupp SMulZeroClass.toSMul instZero smulZeroClass preorder	—	SMulPosMono.lift Pi.instSMulPosMono coe_le_coe coe_smul coe_zero
instSMulPosReflectLE 📖	mathematical	—	SMulPosReflectLE Finsupp SMulZeroClass.toSMul instZero smulZeroClass preorder	—	SMulPosReflectLE.lift Pi.instSMulPosReflectLE coe_le_coe coe_smul coe_zero
instSMulPosReflectLT 📖	mathematical	—	SMulPosReflectLT Finsupp SMulZeroClass.toSMul instZero smulZeroClass SMulWithZero.toSMulZeroClass PartialOrder.toPreorder preorder	—	SMulPosReflectLT.lift Pi.instSMulPosReflectLT coe_le_coe coe_smul coe_zero
instSMulPosStrictMono 📖	mathematical	—	SMulPosStrictMono Finsupp SMulZeroClass.toSMul instZero smulZeroClass SMulWithZero.toSMulZeroClass PartialOrder.toPreorder preorder	—	SMulPosStrictMono.lift Pi.instSMulPosStrictMono coe_le_coe coe_smul coe_zero
isOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid partialorder	—	add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono
isOrderedCancelAddMonoid 📖	mathematical	—	IsOrderedCancelAddMonoid Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid partialorder	—	isOrderedAddMonoid IsOrderedCancelAddMonoid.toIsOrderedAddMonoid le_of_add_le_add_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsOrderedCancelAddMonoid.toAddLeftReflectLT
le_iff 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE PartialOrder.toPreorder DFunLike.coe instFunLike	—	le_iff' Finset.Subset.refl
le_iff' 📖	mathematical	Finset Finset.instHasSubset support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Finsupp instLE Preorder.toLE PartialOrder.toPreorder DFunLike.coe instFunLike	—	zero_le notMem_support_iff
mapDomain_mono 📖	mathematical	—	Monotone Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid preorder PartialOrder.toPreorder mapDomain	—	sum_le_sum_index isOrderedAddMonoid single_mono single_zero
mapDomain_nonneg 📖	mathematical	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE PartialOrder.toPreorder instZero	mapDomain	—	mapDomain_zero mapDomain_mono
mapDomain_nonpos 📖	mathematical	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE PartialOrder.toPreorder instZero	mapDomain	—	mapDomain_zero mapDomain_mono
orderedSub 📖	mathematical	—	OrderedSub Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE PartialOrder.toPreorder instAdd tsub	—	tsub_le_iff_right
single_le_iff 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE PartialOrder.toPreorder single DFunLike.coe instFunLike	—	le_iff' support_single_subset single_eq_same
single_le_single 📖	mathematical	—	Finsupp instLE Preorder.toLE single	—	Pi.single_le_single
single_mono 📖	mathematical	—	Monotone Finsupp preorder single	—	single_le_single
single_nonneg 📖	mathematical	—	Finsupp instLE Preorder.toLE instZero single	—	Pi.single_nonneg
single_nonpos 📖	mathematical	—	Finsupp instLE Preorder.toLE single instZero	—	Pi.single_nonpos
single_tsub 📖	mathematical	—	single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp tsub	—	ext eq_or_ne tsub_apply single_eq_same single_eq_of_ne tsub_self
sub_add_single_one_cancel 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid tsub Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Nat.instOrderedSub single	—	Nat.instCanonicallyOrderedAdd Nat.instOrderedSub sub_single_one_add add_tsub_cancel_right orderedSub addLeftReflectLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
sub_single_one_add 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid tsub Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Nat.instOrderedSub single	—	tsub_add_eq_add_tsub CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAddOfAddLeftMono Nat.instCanonicallyOrderedAdd Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid isOrderedAddMonoid orderedSub addLeftReflectLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le single_le_iff
subset_support_tsub 📖	mathematical	—	Finset Finset.instHasSubset Finset.instSDiff support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp tsub	—	tsub_zero
sum_le_sum 📖	mathematical	Preorder.toLE PartialOrder.toPreorder DFunLike.coe Finsupp instFunLike	sum	—	Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono
sum_le_sum_index 📖	mathematical	Finsupp instLE Preorder.toLE Monotone PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	sum	—	sum_of_support_subset Finset.subset_union_left Finset.subset_union_right Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono
sum_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe Finsupp instFunLike	sum	—	Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono
sum_nonneg' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe Finsupp instFunLike	sum	—	sum_nonneg
sum_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder DFunLike.coe Finsupp instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	sum	—	Finset.sum_nonpos IsOrderedAddMonoid.toAddLeftMono
sum_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe Finsupp instFunLike	sum	—	Finset.sum_pos
sum_pos' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe Finsupp instFunLike Finset Finset.instMembership support Preorder.toLT	sum	—	Finset.sum_pos'
support_inf 📖	mathematical	—	support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp SemilatticeInf.toMin semilatticeInf Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset Finset.instInter	—	Finset.ext
support_mono 📖	mathematical	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE PartialOrder.toPreorder	Finset Finset.instHasSubset support	—	support_monotone
support_monotone 📖	mathematical	—	Monotone Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset preorder PartialOrder.toPreorder Finset.partialOrder support	—	mem_support_iff pos_iff_ne_zero LT.lt.trans_le
support_sup 📖	mathematical	—	support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp SemilatticeSup.toMax semilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset Finset.instUnion	—	Finset.ext
support_tsub 📖	mathematical	—	Finset Finset.instHasSubset support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp tsub	—	—
tsub_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike tsub	—	—

---

← Back to Index