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, embDomain_le_embDomain_iff_le, embDomain_lt_embDomain_iff_lt, embDomain_mono, embDomain_tsub, instCanonicallyOrderedAddOfAddLeftMono, instPosSMulMono, instPosSMulReflectLE, instPosSMulStrictMono, instSMulPosMono, instSMulPosReflectLE, instSMulPosReflectLT, instSMulPosStrictMono, isLowerSet_range_embDomain, isOrderedAddMonoid, isOrderedCancelAddMonoid, le_iff, le_iff', mapDomain_le_mapDomain_iff_le, mapDomain_lt_mapDomain_iff_lt, mapDomain_mono, mapDomain_nonneg, mapDomain_nonpos, mapDomain_tsub, orderedSub, single_eval_le_sum, single_le_iff, single_le_single, single_le_sum, 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	54
Total	58

Finsupp

Definitions

Name	Category	Theorems
decidableLE 📖	CompOp	5 math math: MvPowerSeries.coeff_mul_monomial, MvPowerSeries.coeff_monomial_mul, MvPolynomial.coeff_monomial_mul', MvPowerSeries.coeff_trunc', MvPolynomial.coeff_mul_monomial'
decidableLT 📖	CompOp	4 math math: MvPowerSeries.coeff_inv, MvPowerSeries.coeff_inv_aux, MvPowerSeries.coeff_trunc, MvPowerSeries.coeff_invOfUnit
orderBot 📖	CompOp	10 math math: bot_eq_zero, disjoint_iff, Nat.properDivisors_eq_image_Iio_factorization_prod_pow, Nat.divisors_eq_map_attach_Iic_factorization_prod_pow, Nat.Iio_factorization_prod_pow_injective, card_Iic, card_Iio, Nat.properDivisors_eq_map_attach_Iio_factorization_prod_pow, Nat.Iic_factorization_prod_pow_injective, Nat.divisors_eq_image_Iic_factorization_prod_pow
tsub 📖	CompOp	29 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, embDomain_tsub, coe_tsub, orderedSub, MvPolynomial.coeff_mul_monomial', sub_single_one_add, support_tsub, mapDomain_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	—	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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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
embDomain_le_embDomain_iff_le 📖	mathematical	—	Finsupp instLE embDomain	—	le_def embDomain_apply Function.instEmbeddingLikeEmbedding Classical.choose_eq apply_dite₂
embDomain_lt_embDomain_iff_lt 📖	mathematical	—	Finsupp Preorder.toLT preorder embDomain	—	instReflLe
embDomain_mono 📖	mathematical	—	Monotone Finsupp preorder embDomain	—	embDomain_le_embDomain_iff_le instReflLe
embDomain_tsub 📖	mathematical	—	embDomain AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp tsub	—	embDomain_eq_mapDomain mapDomain_tsub Function.Embedding.injective
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
isLowerSet_range_embDomain 📖	mathematical	—	IsLowerSet Finsupp MulZeroClass.toZero Nat.instMulZeroClass instLE Set.range embDomain	—	ExistsAddOfLE.exists_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAddOfAddLeftMono Nat.instCanonicallyOrderedAdd Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid mem_range_embDomain_iff Finset.coe_map Set.preimage_range
isOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid preorder	—	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 preorder	—	isOrderedAddMonoid IsOrderedCancelAddMonoid.toIsOrderedAddMonoid le_of_add_le_add_left IsOrderedCancelAddMonoid.toAddLeftReflectLE
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 AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE PartialOrder.toPreorder DFunLike.coe instFunLike	—	zero_le notMem_support_iff
mapDomain_le_mapDomain_iff_le 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE mapDomain	—	embDomain_eq_mapDomain embDomain_le_embDomain_iff_le
mapDomain_lt_mapDomain_iff_lt 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLT preorder mapDomain	—	embDomain_eq_mapDomain embDomain_lt_embDomain_iff_lt
mapDomain_mono 📖	mathematical	—	Monotone Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid preorder 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 instZero	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE instZero mapDomain	—	mapDomain_zero mapDomain_mono
mapDomain_nonpos 📖	mathematical	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE instZero	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE mapDomain instZero	—	mapDomain_zero mapDomain_mono
mapDomain_tsub 📖	mathematical	—	mapDomain Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid tsub	—	ext mapDomain_notin_range tsub_self mapDomain_apply
orderedSub 📖	mathematical	—	OrderedSub Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE PartialOrder.toPreorder instAdd tsub	—	tsub_le_iff_right
single_eval_le_sum 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instZero	Preorder.toLE PartialOrder.toPreorder DFunLike.coe Finsupp instFunLike sum	—	sum_single_index single_le_sum
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_le_sum 📖	mathematical	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE PartialOrder.toPreorder sum single DFunLike.coe Finsupp instFunLike	—	eq_or_ne single_zero sum_zero_index sum_nonneg' sum.eq_1 support_single_ne_zero Finset.sum_singleton single_eq_same Finset.single_le_sum IsOrderedAddMonoid.toAddLeftMono
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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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 DFunLike.coe Finsupp instFunLike	Preorder.toLE sum	—	Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono
sum_le_sum_index 📖	mathematical	Finsupp instLE Preorder.toLE Monotone AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE sum	—	sum_of_support_subset Finset.subset_union_left Finset.subset_union_right Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono
sum_nonneg 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe Finsupp instFunLike	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum	—	Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono
sum_nonneg' 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe Finsupp instFunLike	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum	—	sum_nonneg
sum_nonpos 📖	mathematical	Preorder.toLE DFunLike.coe Finsupp instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_nonpos IsOrderedAddMonoid.toAddLeftMono
sum_pos 📖	mathematical	Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe Finsupp instFunLike	Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum	—	Finset.sum_pos
sum_pos' 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe Finsupp instFunLike Finset SetLike.instMembership Finset.instSetLike support Preorder.toLT	Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid 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 AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	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