Documentation Verification Report

Finsupp

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

Statistics

Metric	Count
Definitions `instLE`, `lattice`, `orderEmbeddingToFun`, `orderIsoFunOnFinite`, `partialorder`, `preorder`, `semilatticeInf`, `semilatticeSup`	8
Theorems `coe_le_coe`, `coe_lt_coe`, `coe_mono`, `coe_strictMono`, `inf_apply`, `le_def`, `lt_def`, `orderEmbeddingToFun_apply`, `sup_apply`, `support_inf_union_support_sup`, `support_sup_union_support_inf`	11
Total	19

Finsupp

Definitions

Name	Category	Theorems
`instLE` 📖	CompOp	38 math math: `MvPolynomial.dvd_monomial_one_iff_exists`, `instCanonicallyOrderedAddOfAddLeftMono`, `MvPowerSeries.coeff_mul_monomial`, `coe_le_coe`, `Nat.factorization_le_factorization_mul_left`, `MvPowerSeries.coeff_monomial_mul`, `bot_eq_zero`, `MvPowerSeries.LinearTopology.basis_le_iff`, `MonomialOrder.div_single`, `le_def`, `le_iff`, `StdSimplex.nonneg`, `exists_le_degree_eq`, `MvPolynomial.dvd_monomial_iff_exists`, `single_le_single`, `MvPolynomial.coeff_monomial_mul'`, `MvPowerSeries.coeff_trunc'`, `single_nonpos`, `lt_def`, `orderEmbeddingToFun_apply`, `MvPowerSeries.coeff_truncFun'`, `Nat.factorization_le_iff_dvd`, `coe_orderIsoMultiset_symm`, `wellQuasiOrderedLE`, `MvPolynomial.dvd_monomial_mul_iff_exists`, `MonomialOrder.div_set`, `le_iff'`, `Nat.factorization_le_factorization_mul_right`, `addLeftReflectLE`, `single_le_iff`, `MvPolynomial.monomial_one_dvd_monomial_one`, `orderedSub`, `MonomialOrder.div`, `MvPolynomial.mem_ideal_span_monomial_image`, `MvPolynomial.coeff_mul_monomial'`, `single_nonneg`, `coe_orderIsoMultiset`, `MvPolynomial.monomial_dvd_monomial`
`lattice` 📖	CompOp	1 math math: `card_uIcc`
`orderEmbeddingToFun` 📖	CompOp	1 math math: `orderEmbeddingToFun_apply`
`orderIsoFunOnFinite` 📖	CompOp	—
`partialorder` 📖	CompOp	20 math math: `HahnSeries.instNoZeroDivisorsFinsuppNat`, `floorDiv_def`, `isOrderedAddMonoid`, `coe_ceilDiv_def`, `disjoint_iff`, `HahnSeries.toMvPowerSeries_symm_apply_coeff`, `isOrderedCancelAddMonoid`, `floorDiv_apply`, `ceilDiv_apply`, `ceilDiv_def`, `Nat.ceilRoot_def`, `support_ceilDiv_subset`, `Nat.factorization_ceilRoot`, `support_floorDiv_subset`, `HahnSeries.coeff_toMvPowerSeries_symm`, `Nat.factorization_floorRoot`, `coe_floorDiv`, `Nat.floorRoot_def`, `HahnSeries.coeff_toMvPowerSeries`, `HahnSeries.toMvPowerSeries_apply`
`preorder` 📖	CompOp	43 math math: `instSMulPosReflectLE`, `MvPowerSeries.WithPiTopology.tendsto_trunc_atTop`, `instPosSMulReflectLE`, `MvPowerSeries.eq_iff_frequently_trunc'_eq`, `card_Ioc`, `toMultiset_strictMono`, `card_Ico`, `toColex_monotone`, `MvPolynomial.pow_idealOfVars`, `MvPolynomial.idealOfVars_eq_restrictSupportIdeal`, `MonomialOrder.toSyn_strictMono`, `MvPowerSeries.coeff_inv`, `mapDomain_mono`, `card_Icc`, `instSMulPosReflectLT`, `card_Ioo`, `instSMulPosMono`, `coe_strictMono`, `instPosSMulStrictMono`, `wellFoundedLT'`, `isPWO`, `single_mono`, `MonomialOrder.toSyn_monotone`, `MvPowerSeries.coeff_inv_aux`, `lt_def`, `MvPowerSeries.coeff_trunc`, `instPosSMulMono`, `MvPowerSeries.coeff_truncFun`, `wellFoundedLT`, `instSMulPosStrictMono`, `MvPowerSeries.coeff_invOfUnit`, `coe_lt_coe`, `card_Iic`, `MvPowerSeries.WithPiTopology.tendsto_trunc'_atTop`, `card_Iio`, `Icc_eq`, `support_monotone`, `degree_mono`, `toLex_monotone`, `coe_mono`, `wellFoundedLT_of_finite`, `Multiset.toFinsupp_strictMono`, `lt_wf`
`semilatticeInf` 📖	CompOp	7 math math: `Multiset.toFinsupp_inter`, `inf_apply`, `support_inf_union_support_sup`, `support_sup_union_support_inf`, `support_inf`, `Nat.factorization_gcd`, `toMultiset_inf`
`semilatticeSup` 📖	CompOp	17 math math: `MonomialOrder.sPolynomial_leadingTerm_mul'`, `Multiset.toFinsupp_union`, `MonomialOrder.sPolynomial_def`, `Nat.factorization_lcm`, `MonomialOrder.sPolynomial_monomial_mul`, `sup_apply`, `support_inf_union_support_sup`, `MonomialOrder.sPolynomial_monomial_mul'`, `support_sup`, `MonomialOrder.degree_sPolynomial_le`, `MonomialOrder.coeff_sPolynomial_sup_eq_zero`, `support_sup_union_support_inf`, `toMultiset_sup`, `MonomialOrder.degree_sPolynomial_lt_sup_degree`, `MonomialOrder.sPolynomial_mul_monomial`, `MonomialOrder.sPolynomial_leadingTerm_mul`, `MonomialOrder.degree_sPolynomial`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_le_coe` 📖	mathematical	—	`Pi.hasLe` `DFunLike.coe` `Finsupp` `instFunLike` `instLE`	—	—
`coe_lt_coe` 📖	mathematical	—	`Preorder.toLT` `Pi.preorder` `DFunLike.coe` `Finsupp` `instFunLike` `preorder`	—	—
`coe_mono` 📖	mathematical	—	`Monotone` `Finsupp` `preorder` `Pi.preorder` `toFun`	—	—
`coe_strictMono` 📖	mathematical	—	`Monotone` `Finsupp` `preorder` `Pi.preorder` `toFun`	—	—
`inf_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `SemilatticeInf.toMin` `semilatticeInf`	—	—
`le_def` 📖	mathematical	—	`Finsupp` `instLE` `DFunLike.coe` `instFunLike`	—	—
`lt_def` 📖	mathematical	—	`Finsupp` `Preorder.toLT` `preorder` `instLE` `Preorder.toLE` `DFunLike.coe` `instFunLike`	—	`Pi.lt_def`
`orderEmbeddingToFun_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Finsupp` `instLE` `Pi.hasLe` `RelEmbedding.instFunLike` `orderEmbeddingToFun` `instFunLike`	—	—
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `SemilatticeSup.toMax` `semilatticeSup`	—	—
`support_inf_union_support_sup` 📖	mathematical	—	`Finset` `Finset.instUnion` `support` `Finsupp` `SemilatticeInf.toMin` `semilatticeInf` `Lattice.toSemilatticeInf` `SemilatticeSup.toMax` `semilatticeSup` `Lattice.toSemilatticeSup`	—	`Finset.coe_injective` `compl_injective` `Set.ext` `Finset.coe_union` `Set.compl_union`
`support_sup_union_support_inf` 📖	mathematical	—	`Finset` `Finset.instUnion` `support` `Finsupp` `SemilatticeSup.toMax` `semilatticeSup` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin` `semilatticeInf` `Lattice.toSemilatticeInf`	—	`Finset.union_comm` `support_inf_union_support_sup`

---

← Back to Index