Order

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

Statistics

Metric	Count
Definitions decidableLE, instLE, instOrderBot, instPartialOrder, instPreorder, instSemilatticeInf, instSemilatticeSup, lattice, orderEmbeddingToFun, tsub	10
Theorems add_eq_zero_iff, bot_eq_zero, coe_inf, coe_le_coe, coe_lt_coe, coe_mono, coe_orderEmbeddingToFun, coe_strictMono, coe_sup, coe_tsub, disjoint_iff, inf_apply, instAddLeftReflectLE, instCanonicallyOrderedAddOfAddLeftMono, instIsOrderedAddMonoid, instIsOrderedCancelAddMonoid, instOrderedSub, instPosSMulMono, instPosSMulReflectLE, instPosSMulStrictMono, instSMulPosMono, instSMulPosReflectLE, instSMulPosReflectLT, instSMulPosStrictMono, le_def, le_iff, le_iff', lt_def, orderEmbeddingToFun_apply, single_le_iff, single_tsub, subset_support_tsub, sup_apply, support_inf, support_inf_union_support_sup, support_mono, support_monotone, support_sup, support_sup_union_support_inf, support_tsub, tsub_apply	41
Total	51

DFinsupp

Definitions

Name	Category	Theorems
decidableLE 📖	CompOp	—
instLE 📖	CompOp	14 math math: lt_def, le_iff', single_le_iff, le_def, instCanonicallyOrderedAddOfAddLeftMono, toMultiset_le_toMultiset, le_iff, coe_orderEmbeddingToFun, instAddLeftReflectLE, bot_eq_zero, instOrderedSub, Multiset.toDFinsupp_le_toDFinsupp, coe_le_coe, orderEmbeddingToFun_apply
instOrderBot 📖	CompOp	4 math math: disjoint_iff, card_Iic, bot_eq_zero, card_Iio
instPartialOrder 📖	CompOp	1 math math: disjoint_iff
instPreorder 📖	CompOp	29 math math: instIsOrderedCancelAddMonoid, coe_mono, toLex_monotone, Multiset.Icc_eq, lt_def, instSMulPosMono, card_Iic, wellFoundedLT', wellFoundedLT, instPosSMulStrictMono, card_Ioo, Icc_eq, instPosSMulReflectLE, instPosSMulMono, instSMulPosReflectLT, coe_strictMono, card_Ico, toColex_monotone, instSMulPosReflectLE, instIsOrderedAddMonoid, Multiset.toDFinsupp_lt_toDFinsupp, toMultiset_lt_toMultiset, card_Iio, coe_lt_coe, card_Icc, card_Ioc, wellFoundedLT_of_finite, instSMulPosStrictMono, support_monotone
instSemilatticeInf 📖	CompOp	7 math math: support_inf, toMultiset_inf, inf_apply, support_sup_union_support_inf, coe_inf, Multiset.toDFinsupp_inter, support_inf_union_support_sup
instSemilatticeSup 📖	CompOp	7 math math: toMultiset_sup, coe_sup, sup_apply, support_sup_union_support_inf, Multiset.toDFinsupp_union, support_inf_union_support_sup, support_sup
lattice 📖	CompOp	2 math math: Multiset.uIcc_eq, card_uIcc
orderEmbeddingToFun 📖	CompOp	2 math math: coe_orderEmbeddingToFun, orderEmbeddingToFun_apply
tsub 📖	CompOp	6 math math: tsub_apply, coe_tsub, subset_support_tsub, support_tsub, single_tsub, instOrderedSub

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_zero_iff 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAdd instZero	—	Unique.instSubsingleton
bot_eq_zero 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	Bot.bot DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid OrderBot.toBot instLE Preorder.toLE PartialOrder.toPreorder instOrderBot instZero	—	—
coe_inf 📖	mathematical	—	DFunLike.coe DFinsupp instDFunLike SemilatticeInf.toMin instSemilatticeInf Pi.instMinForall_mathlib	—	—
coe_le_coe 📖	mathematical	—	Pi.hasLe DFunLike.coe DFinsupp instDFunLike instLE	—	—
coe_lt_coe 📖	mathematical	—	Preorder.toLT Pi.preorder DFunLike.coe DFinsupp instDFunLike instPreorder	—	—
coe_mono 📖	mathematical	—	Monotone DFinsupp instPreorder Pi.preorder DFunLike.coe instDFunLike	—	—
coe_orderEmbeddingToFun 📖	mathematical	—	DFunLike.coe OrderEmbedding DFinsupp instLE Pi.hasLe instFunLikeOrderEmbedding orderEmbeddingToFun instDFunLike	—	—
coe_strictMono 📖	mathematical	—	Monotone DFinsupp instPreorder Pi.preorder DFunLike.coe instDFunLike	—	—
coe_sup 📖	mathematical	—	DFunLike.coe DFinsupp instDFunLike SemilatticeSup.toMax instSemilatticeSup Pi.instMaxForall_mathlib	—	—
coe_tsub 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instDFunLike tsub Pi.instSub	—	tsub_apply
disjoint_iff 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Disjoint DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instPartialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instOrderBot Finset Finset.partialOrder Finset.instOrderBot support LinearOrder.toDecidableEq	—	disjoint_iff bot_eq_zero support_eq_empty support_inf
inf_apply 📖	mathematical	—	DFunLike.coe DFinsupp instDFunLike SemilatticeInf.toMin instSemilatticeInf	—	zipWith_apply
instAddLeftReflectLE 📖	mathematical	AddLeftReflectLE AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	AddLeftReflectLE DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAdd instLE Preorder.toLE PartialOrder.toPreorder	—	le_of_add_le_add_left
instCanonicallyOrderedAddOfAddLeftMono 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub AddLeftMono	CanonicallyOrderedAdd DFinsupp 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
instIsOrderedAddMonoid 📖	mathematical	IsOrderedAddMonoid PartialOrder.toPreorder	IsOrderedAddMonoid DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid instPreorder PartialOrder.toPreorder	—	add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono
instIsOrderedCancelAddMonoid 📖	mathematical	IsOrderedCancelAddMonoid PartialOrder.toPreorder	IsOrderedCancelAddMonoid DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid instPreorder PartialOrder.toPreorder	—	instIsOrderedAddMonoid IsOrderedCancelAddMonoid.toIsOrderedAddMonoid le_of_add_le_add_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLT
instOrderedSub 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub	OrderedSub DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE PartialOrder.toPreorder instAdd tsub	—	tsub_le_iff_right
instPosSMulMono 📖	mathematical	PosSMulMono SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	PosSMulMono DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul instZero instSMulZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	PosSMulMono.lift Pi.instPosSMulMono coe_le_coe coe_smul
instPosSMulReflectLE 📖	mathematical	PosSMulReflectLE SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	PosSMulReflectLE DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul instZero instSMulZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	PosSMulReflectLE.lift Pi.instPosSMulReflectLE coe_le_coe coe_smul
instPosSMulStrictMono 📖	mathematical	PosSMulStrictMono SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	PosSMulStrictMono DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul instZero instSMulZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PartialOrder.toPreorder instPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	PosSMulStrictMono.lift Pi.instPosSMulStrictMono coe_le_coe coe_smul
instSMulPosMono 📖	mathematical	SMulPosMono SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	SMulPosMono DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul instZero instSMulZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instPreorder	—	SMulPosMono.lift Pi.instSMulPosMono coe_le_coe coe_smul coe_zero
instSMulPosReflectLE 📖	mathematical	SMulPosReflectLE SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	SMulPosReflectLE DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul instZero instSMulZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instPreorder	—	SMulPosReflectLE.lift Pi.instSMulPosReflectLE coe_le_coe coe_smul coe_zero
instSMulPosReflectLT 📖	mathematical	SMulPosReflectLT SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PartialOrder.toPreorder	SMulPosReflectLT DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul instZero instSMulZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PartialOrder.toPreorder instPreorder	—	SMulPosReflectLT.lift Pi.instSMulPosReflectLT coe_le_coe coe_smul coe_zero
instSMulPosStrictMono 📖	mathematical	SMulPosStrictMono SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PartialOrder.toPreorder	SMulPosStrictMono DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul instZero instSMulZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PartialOrder.toPreorder instPreorder	—	SMulPosStrictMono.lift Pi.instSMulPosStrictMono coe_le_coe coe_smul coe_zero
le_def 📖	mathematical	—	DFinsupp instLE DFunLike.coe instDFunLike	—	—
le_iff 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE PartialOrder.toPreorder DFunLike.coe instDFunLike	—	le_iff' Finset.Subset.refl
le_iff' 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder Finset Finset.instHasSubset support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE PartialOrder.toPreorder DFunLike.coe instDFunLike	—	zero_le notMem_support_iff
lt_def 📖	mathematical	—	DFinsupp Preorder.toLT instPreorder instLE Preorder.toLE DFunLike.coe instDFunLike	—	Pi.lt_def
orderEmbeddingToFun_apply 📖	mathematical	—	DFunLike.coe OrderEmbedding DFinsupp instLE Pi.hasLe instFunLikeOrderEmbedding orderEmbeddingToFun instDFunLike	—	—
single_le_iff 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE Preorder.toLE PartialOrder.toPreorder single DFunLike.coe instDFunLike	—	le_iff' support_single_subset single_apply
single_tsub 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub	single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp tsub	—	ext eq_or_ne tsub_apply single_eq_same single_eq_of_ne tsub_self
subset_support_tsub 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub	Finset Finset.instHasSubset Finset.instSDiff support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp tsub	—	coe_tsub tsub_zero
sup_apply 📖	mathematical	—	DFunLike.coe DFinsupp instDFunLike SemilatticeSup.toMax instSemilatticeSup	—	zipWith_apply
support_inf 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearOrder.toDecidableEq DFinsupp SemilatticeInf.toMin instSemilatticeInf Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset Finset.instInter	—	Finset.ext inf_apply
support_inf_union_support_sup 📖	mathematical	—	Finset Finset.instUnion support DFinsupp SemilatticeInf.toMin instSemilatticeInf Lattice.toSemilatticeInf SemilatticeSup.toMax instSemilatticeSup Lattice.toSemilatticeSup	—	Finset.coe_injective compl_injective Set.ext Finset.coe_union Set.compl_union
support_mono 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE	Finset Finset.instHasSubset support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	support_monotone
support_monotone 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	Monotone DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instPreorder PartialOrder.toPreorder Finset.partialOrder support	—	mem_support_iff pos_iff_ne_zero LT.lt.trans_le
support_sup 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearOrder.toDecidableEq DFinsupp SemilatticeSup.toMax instSemilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset Finset.instUnion	—	Finset.ext sup_apply
support_sup_union_support_inf 📖	mathematical	—	Finset Finset.instUnion support DFinsupp SemilatticeSup.toMax instSemilatticeSup Lattice.toSemilatticeSup SemilatticeInf.toMin instSemilatticeInf Lattice.toSemilatticeInf	—	Finset.union_comm support_inf_union_support_sup
support_tsub 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub	Finset Finset.instHasSubset support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp tsub	—	coe_tsub
tsub_apply 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instDFunLike tsub	—	zipWith_apply

---

← Back to Index