Order

📁 Source: Mathlib/RingTheory/PowerSeries/Order.lean

Statistics

Metric	Count
Definitions `divXPowOrder`, `divXPowOrderHom`, `orderHom`	3
Theorems `X_pow_order_dvd`, `X_pow_order_mul_divXPowOrder`, `coe_divXPowOrderHom`, `coe_orderHom`, `coe_toNat_order`, `coeff_divXPowOrder`, `coeff_mul_of_lt_order`, `coeff_mul_one_sub_of_lt_order`, `coeff_mul_prod_one_sub_of_lt_order`, `coeff_of_lt_order`, `coeff_of_lt_order_toNat`, `coeff_order`, `constantCoeff_divXPowOrder`, `constantCoeff_divXPowOrder_eq_zero_iff`, `divXPowOrder_X`, `divXPowOrder_mul`, `divXPowOrder_mul_divXPowOrder`, `divXPowOrder_one`, `divXPowOrder_pow`, `divXPowOrder_prod`, `divXPowOrder_zero`, `exists_coeff_ne_zero_iff_ne_zero`, `le_order`, `le_order_map`, `le_order_mul`, `le_order_pow`, `le_order_pow_of_constantCoeff_eq_zero`, `le_order_prod`, `le_order_smul`, `min_order_le_order_add`, `nat_le_order`, `one_le_order_iff_constCoeff_eq_zero`, `order_X`, `order_X_pow`, `order_add_of_order_eq`, `order_add_of_order_ne`, `order_eq`, `order_eq_emultiplicity_X`, `order_eq_nat`, `order_eq_order`, `order_eq_top`, `order_finite_iff_ne_zero`, `order_le`, `order_monomial`, `order_monomial_of_ne_zero`, `order_mul`, `order_mul_ge`, `order_ne_zero_iff_constCoeff_eq_zero`, `order_neg`, `order_one`, `order_pow`, `order_prod`, `order_toSubring`, `order_zero`, `order_zero_of_unit`	55
Total	58

PowerSeries

Definitions

Name	Category	Theorems
`divXPowOrder` 📖	CompOp	17 math math: `eq_divided_by_X_pow_order_Iff_Unit`, `Inv_divided_by_X_pow_order_leftInv`, `divXPowOrder_prod`, `divXPowOrder_mul`, `isUnit_divided_by_X_pow_order`, `divXPowOrder_one`, `coe_divXPowOrderHom`, `constantCoeff_divXPowOrder`, `divXPowOrder_mul_divXPowOrder`, `constantCoeff_divXPowOrder_eq_zero_iff`, `Unit_of_divided_by_X_pow_order_nonzero`, `divXPowOrder_pow`, `coeff_divXPowOrder`, `X_pow_order_mul_divXPowOrder`, `Inv_divided_by_X_pow_order_rightInv`, `divXPowOrder_X`, `divXPowOrder_zero`
`divXPowOrderHom` 📖	CompOp	1 math math: `coe_divXPowOrderHom`
`orderHom` 📖	CompOp	1 math math: `coe_orderHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`X_pow_order_dvd` 📖	mathematical	—	`PowerSeries` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `instSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `ENat.toNat` `order`	—	`coeff_of_lt_order_toNat`
`X_pow_order_mul_divXPowOrder` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `X` `ENat.toNat` `order` `divXPowOrder`	—	`ext` `coeff_X_pow_mul'` `coeff_divXPowOrder` `coeff_of_lt_order_toNat`
`coe_divXPowOrderHom` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `PowerSeries` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `instSemiring` `MonoidHom.instFunLike` `divXPowOrderHom` `divXPowOrder`	—	—
`coe_orderHom` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `PowerSeries` `Multiplicative` `ENat` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `instSemiring` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `CommSemiring.toSemiring` `instCommSemiringENat` `MonoidHom.instFunLike` `orderHom` `order`	—	—
`coe_toNat_order` 📖	mathematical	—	`ENat` `ENat.instNatCast` `ENat.toNat` `order`	—	`ENat.coe_toNat_eq_self` `Iff.not` `order_eq_top`
`coeff_divXPowOrder` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `divXPowOrder` `ENat.toNat` `order`	—	—
`coeff_mul_of_lt_order` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `order`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MvPowerSeries.instMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`coeff_mul` `Finset.sum_congr` `mul_eq_zero_of_right` `coeff_of_lt_order` `lt_of_le_of_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Finset.HasAntidiagonal.mem_antidiagonal` `Finset.sum_const_zero`
`coeff_mul_one_sub_of_lt_order` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `order` `Ring.toSemiring`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MvPowerSeries.instMul` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `MvPowerSeries.instOne`	—	`mul_sub` `mul_one` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `coeff_mul_of_lt_order` `sub_zero`
`coeff_mul_prod_one_sub_of_lt_order` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `order` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MvPowerSeries.instMul` `Finset.prod` `CommRing.toCommMonoid` `instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPowerSeries.instOne`	—	`Finset.induction_on` `instIsEmptyFalse` `mul_one` `Finset.prod_insert` `mul_assoc` `mul_right_comm` `coeff_mul_one_sub_of_lt_order`
`coeff_of_lt_order` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `order`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `order_le`
`coeff_of_lt_order_toNat` 📖	mathematical	`ENat.toNat` `order`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `coeff_of_lt_order` `coe_toNat_order` `ENat.coe_lt_coe`
`coeff_order` 📖	—	—	—	—	`Nat.find_spec`
`constantCoeff_divXPowOrder` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `constantCoeff` `divXPowOrder` `LinearMap` `RingHom.id` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `ENat.toNat` `order`	—	`coeff_divXPowOrder` `zero_add`
`constantCoeff_divXPowOrder_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `constantCoeff` `divXPowOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instZero`	—	`divXPowOrder_zero` `constantCoeff_divXPowOrder` `coeff_order`
`divXPowOrder_X` 📖	mathematical	—	`divXPowOrder` `X` `PowerSeries` `MvPowerSeries.instOne`	—	`ext` `coeff_divXPowOrder` `order_X` `coeff_X` `coeff_one`
`divXPowOrder_mul` 📖	mathematical	—	`divXPowOrder` `PowerSeries` `MvPowerSeries.instMul`	—	`MulZeroClass.zero_mul` `divXPowOrder_zero` `MulZeroClass.mul_zero` `X_pow_mul_cancel` `order_mul` `ENat.toNat_add` `Iff.not` `order_eq_top` `X_pow_order_mul_divXPowOrder` `mul_assoc` `X_pow_mul` `pow_add` `add_comm`
`divXPowOrder_mul_divXPowOrder` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `divXPowOrder`	—	`divXPowOrder_mul`
`divXPowOrder_one` 📖	mathematical	—	`divXPowOrder` `PowerSeries` `MvPowerSeries.instOne`	—	`ext` `coeff_divXPowOrder` `order_one` `add_zero` `coeff_one`
`divXPowOrder_pow` 📖	mathematical	—	`divXPowOrder` `PowerSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`map_pow` `MonoidHom.instMonoidHomClass`
`divXPowOrder_prod` 📖	mathematical	—	`divXPowOrder` `CommSemiring.toSemiring` `Finset.prod` `PowerSeries` `CommSemiring.toCommMonoid` `instCommSemiring`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`divXPowOrder_zero` 📖	mathematical	—	`divXPowOrder` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`ext` `coeff_divXPowOrder` `order_zero` `add_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`exists_coeff_ne_zero_iff_ne_zero` 📖	—	—	—	—	`Mathlib.Tactic.Contrapose.contrapose_iff₃`
`le_order` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `order`	—	`ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `nat_le_order` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`le_order_map` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `order` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `map`	—	`le_order` `coeff_of_lt_order` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`le_order_mul` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `order` `PowerSeries` `MvPowerSeries.instMul`	—	`le_order` `coeff_mul` `Finset.sum_eq_zero` `coeff_of_lt_order` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `ne_of_lt` `lt_of_lt_of_le` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Nat.cast_add` `Finset.HasAntidiagonal.mem_antidiagonal`
`le_order_pow` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `order` `PowerSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`zero_nsmul` `pow_zero` `add_smul` `one_smul` `pow_succ` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `le_refl` `le_order_mul`
`le_order_pow_of_constantCoeff_eq_zero` 📖	mathematical	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `constantCoeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `order` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`LE.le.trans` `nsmul_eq_mul` `le_mul_of_one_le_right'` `CanonicallyOrderedAdd.toMulLeftMono` `one_le_order_iff_constCoeff_eq_zero` `le_order_pow`
`le_order_prod` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Finset.sum` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid` `instLinearOrderedAddCommMonoidWithTopENat` `order` `CommSemiring.toSemiring` `Finset.prod` `PowerSeries` `CommSemiring.toCommMonoid` `instCommSemiring`	—	`Finset.cons_induction` `Finset.sum_cons` `Finset.prod_cons` `le_imp_le_of_le_of_le` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `le_refl` `le_order_mul`
`le_order_smul` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `order` `PowerSeries` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule`	—	`le_order` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `coeff_of_lt_order` `MulZeroClass.mul_zero`
`min_order_le_order_add` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `SemilatticeInf.toMin` `order` `PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring`	—	`le_order` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `coeff_of_lt_order` `add_zero`
`nat_le_order` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `order`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`one_le_order_iff_constCoeff_eq_zero` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `order` `DFunLike.coe` `RingHom` `PowerSeries` `instSemiring` `RingHom.instFunLike` `constantCoeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`coeff_zero_eq_constantCoeff` `coeff_of_lt_order` `CharP.cast_eq_zero` `CharP.ofCharZero` `Order.one_le_iff_pos` `IsOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `le_order` `Nat.cast_lt_one` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid`
`order_X` 📖	mathematical	—	`order` `X` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.cast_one` `order_monomial_of_ne_zero` `one_ne_zero` `NeZero.one`
`order_X_pow` 📖	mathematical	—	`order` `PowerSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `X` `ENat` `ENat.instNatCast`	—	`X_pow_eq` `order_monomial_of_ne_zero` `one_ne_zero` `NeZero.one`
`order_add_of_order_eq` 📖	mathematical	—	`order` `PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `ENat` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	—	`order_add_of_order_ne`
`order_add_of_order_ne` 📖	mathematical	—	`order` `PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `ENat` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	—	`le_antisymm` `Ne.lt_or_gt` `add_comm` `inf_comm` `min_order_le_order_add`
`order_eq` 📖	mathematical	—	`order` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`instIsEmptyFalse` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`order_eq_emultiplicity_X` 📖	mathematical	—	`order` `emultiplicity` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `X`	—	`eq_or_ne` `order_zero` `emultiplicity_zero` `le_antisymm` `Order.le_of_lt_add_one` `not_le` `Nat.cast_one` `Nat.cast_add` `pow_dvd_iff_le_emultiplicity` `coeff_order` `coeff_mul_of_lt_order` `X_pow_eq` `order_monomial` `ENat.coe_lt_coe` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass` `X_pow_mul` `le_emultiplicity_of_pow_dvd` `X_pow_order_dvd`
`order_eq_nat` 📖	mathematical	—	`order` `ENat` `ENat.instNatCast` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`eq_or_ne` `order_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`order_eq_order` 📖	mathematical	—	`order` `MvPowerSeries.order`	—	`eq_of_le_of_ge` `MvPowerSeries.le_order` `coeff_of_lt_order` `Finset.sum_eq_single` `instIsEmptyFalse` `coeff_def` `le_order` `MvPowerSeries.coeff_of_lt_order` `Finsupp.degree_single`
`order_eq_top` 📖	mathematical	—	`order` `Top.top` `ENat` `instTopENat` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Iff.not_left` `order_finite_iff_ne_zero`
`order_finite_iff_ne_zero` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `order` `Top.top` `instTopENat`	—	—
`order_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `order` `ENat.instNatCast`	—	`order.eq_1` `exists_coeff_ne_zero_iff_ne_zero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `le_rfl`
`order_monomial` 📖	mathematical	—	`order` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Top.top` `instTopENat` `ENat.instNatCast`	—	`order_eq_top` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `order_eq` `coeff_monomial_same` `coeff_monomial` `ne_of_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`order_monomial_of_ne_zero` 📖	mathematical	—	`order` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `ENat` `ENat.instNatCast`	—	`order_monomial`
`order_mul` 📖	mathematical	—	`order` `PowerSeries` `MvPowerSeries.instMul` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`le_antisymm` `MulZeroClass.zero_mul` `order_zero` `top_add` `MulZeroClass.mul_zero` `add_top` `coe_toNat_order` `ENat.coe_add` `order_le` `coeff_mul` `Finset.sum_eq_single_of_mem` `trichotomy_of_add_eq_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Finset.HasAntidiagonal.mem_antidiagonal` `coeff_of_lt_order_toNat` `mul_ne_zero` `coeff_order` `le_order_mul`
`order_mul_ge` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `order` `PowerSeries` `MvPowerSeries.instMul`	—	`le_order_mul`
`order_ne_zero_iff_constCoeff_eq_zero` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `constantCoeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`ENat.one_le_iff_ne_zero` `one_le_order_iff_constCoeff_eq_zero`
`order_neg` 📖	mathematical	—	`order` `Ring.toSemiring` `PowerSeries` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `Ring.toAddCommGroup`	—	`neg_add_cancel` `order_zero` `order_add_of_order_ne` `neg_zero`
`order_one` 📖	mathematical	—	`order` `PowerSeries` `MvPowerSeries.instOne` `ENat` `instZeroENat`	—	`monomial_zero_eq_C` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `CharP.cast_eq_zero` `CharP.ofCharZero` `order_monomial_of_ne_zero` `one_ne_zero` `NeZero.one`
`order_pow` 📖	mathematical	—	`order` `PowerSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `ENat` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`map_pow` `MonoidHom.instMonoidHomClass`
`order_prod` 📖	mathematical	—	`order` `CommSemiring.toSemiring` `Finset.prod` `PowerSeries` `CommSemiring.toCommMonoid` `instCommSemiring` `Finset.sum` `ENat` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid` `instLinearOrderedAddCommMonoidWithTopENat`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`order_toSubring` 📖	mathematical	`Subring` `SetLike.instMembership` `Subring.instSetLike` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff`	`order` `Subring.toRing` `toSubring`	—	`eq_of_le_of_ge` `le_order` `coeff_toSubring` `coeff_of_lt_order` `Nat.cast_zero`
`order_zero` 📖	mathematical	—	`order` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Top.top` `ENat` `instTopENat`	—	—
`order_zero_of_unit` 📖	mathematical	`IsUnit` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	`order` `ENat` `instZeroENat`	—	`add_eq_zero` `Unique.instSubsingleton` `nonpos_iff_eq_zero` `order_one` `order_mul_ge`

---

← Back to Index