Order

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

Statistics

Metric	Count
Definitions `IsHomogeneous`, `IsWeightedHomogeneous`, `homogeneousComponent`, `weightedHomogeneousComponent`, `weightedOrder`	5
Theorems `add`, `coeff_eq_zero`, `mul`, `add`, `coeff_eq_zero`, `mul`, `coeff_eq_zero_of_lt_weightedOrder`, `coeff_homogeneousComponent`, `coeff_mul_left_one_sub_of_lt_order`, `coeff_mul_left_one_sub_of_lt_weightedOrder`, `coeff_mul_prod_one_sub_of_lt_order`, `coeff_mul_prod_one_sub_of_lt_weightedOrder`, `coeff_mul_right_one_sub_of_lt_order`, `coeff_mul_right_one_sub_of_lt_weightedOrder`, `coeff_of_lt_order`, `coeff_weightedHomogeneousComponent`, `eq_zero_iff_forall_coeff_eq_zero_and`, `exists_coeff_ne_zero_and_order`, `exists_coeff_ne_zero_and_weightedOrder`, `homogeneousComponent_mul_of_le_order`, `homogeneousComponent_of_lt_order_eq_zero`, `homogeneousComponent_of_order`, `isHomogeneous_homogeneousComponent`, `isHomogeneous_iff_eq_homogeneousComponent`, `isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent`, `isWeightedHomogeneous_weightedHomogeneousComponent`, `le_order`, `le_order_map`, `le_order_mul`, `le_order_pow`, `le_order_pow_of_constantCoeff_eq_zero`, `le_order_prod`, `le_order_smul`, `le_weightedOrder`, `le_weightedOrder_map`, `le_weightedOrder_mul`, `le_weightedOrder_pow`, `le_weightedOrder_prod`, `le_weightedOrder_smul`, `min_order_le_add`, `min_weightedOrder_le_add`, `nat_le_order`, `nat_le_weightedOrder`, `ne_zero_iff_exists_coeff_ne_zero_and_degree`, `ne_zero_iff_exists_coeff_ne_zero_and_weight`, `ne_zero_iff_order_finite`, `ne_zero_iff_weightedOrder_finite`, `one_le_order_iff_constCoeff_eq_zero`, `order_add_of_order_ne`, `order_eq_nat`, `order_eq_top_iff`, `order_le`, `order_monomial`, `order_monomial_of_ne_zero`, `order_mul_ge`, `order_ne_zero_iff_constCoeff_eq_zero`, `order_neg`, `order_toSubring`, `order_zero`, `weightedHomogeneousComponent_mul_of_le_weightedOrder`, `weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero`, `weightedHomogeneousComponent_of_weightedOrder`, `weightedOrder_add_of_weightedOrder_ne`, `weightedOrder_eq_nat`, `weightedOrder_eq_top_iff`, `weightedOrder_le`, `weightedOrder_monomial`, `weightedOrder_monomial_of_ne_zero`, `weightedOrder_mul_ge`, `weightedOrder_neg`, `weightedOrder_one`, `weightedOrder_toSubring`, `weightedOrder_zero`	73
Total	78

MvPowerSeries

Definitions

Name	Category	Theorems
`IsHomogeneous` 📖	MathDef	2 math math: `isHomogeneous_iff_eq_homogeneousComponent`, `isHomogeneous_homogeneousComponent`
`IsWeightedHomogeneous` 📖	MathDef	2 math math: `isWeightedHomogeneous_weightedHomogeneousComponent`, `isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent`
`homogeneousComponent` 📖	CompOp	5 math math: `coeff_homogeneousComponent`, `homogeneousComponent_of_lt_order_eq_zero`, `isHomogeneous_iff_eq_homogeneousComponent`, `homogeneousComponent_mul_of_le_order`, `isHomogeneous_homogeneousComponent`
`weightedHomogeneousComponent` 📖	CompOp	5 math math: `weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero`, `coeff_weightedHomogeneousComponent`, `weightedHomogeneousComponent_mul_of_le_weightedOrder`, `isWeightedHomogeneous_weightedHomogeneousComponent`, `isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent`
`weightedOrder` 📖	CompOp	25 math math: `weightedOrder_monomial`, `le_weightedOrder_mul`, `le_weightedOrder_prod`, `weightedOrder_monomial_of_ne_zero`, `weightedOrder_mul`, `le_weightedOrder_map`, `nat_le_weightedOrder`, `le_weightedOrder_pow`, `min_weightedOrder_le_add`, `ne_zero_iff_weightedOrder_finite`, `le_weightedOrder_smul`, `le_weightedOrder_subst`, `weightedOrder_mul_ge`, `weightedOrder_neg`, `weightedOrder_eq_nat`, `weightedOrder_le`, `weightedOrder_add_of_weightedOrder_ne`, `le_weightedOrder`, `weightedOrder_zero`, `weightedOrder_toSubring`, `le_weightedOrder_subst_of_forall_ne_zero`, `weightedOrder_eq_top_iff`, `weightedOrder_prod`, `PowerSeries.le_weightedOrder_subst`, `weightedOrder_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_eq_zero_of_lt_weightedOrder` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule` `weightedOrder`	`LinearMap` `RingHom.id` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `weightedOrder_le`
`coeff_homogeneousComponent` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `homogeneousComponent` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finsupp.degree_eq_weight_one` `coeff_weightedHomogeneousComponent`
`coeff_mul_left_one_sub_of_lt_order` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `order` `Ring.toSemiring`	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `instMul` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instOne`	—	`coeff_mul_left_one_sub_of_lt_weightedOrder` `Finsupp.degree_eq_weight_one`
`coeff_mul_left_one_sub_of_lt_weightedOrder` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule` `weightedOrder` `Ring.toSemiring`	`LinearMap` `RingHom.id` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `instMul` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instOne`	—	`mul_sub` `mul_one` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `coeff_eq_zero_of_lt_weightedOrder` `lt_of_lt_of_le` `le_add_self` `le_weightedOrder_mul`
`coeff_mul_prod_one_sub_of_lt_order` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `order` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `instMul` `Finset.prod` `CommRing.toCommMonoid` `instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instOne`	—	`Finsupp.degree_eq_weight_one` `coeff_mul_prod_one_sub_of_lt_weightedOrder`
`coeff_mul_prod_one_sub_of_lt_weightedOrder` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule` `weightedOrder` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`LinearMap` `RingHom.id` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `instMul` `Finset.prod` `CommRing.toCommMonoid` `instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instOne`	—	`Finset.induction_on` `mul_one` `Finset.prod_insert` `mul_assoc` `mul_right_comm` `coeff_mul_left_one_sub_of_lt_weightedOrder`
`coeff_mul_right_one_sub_of_lt_order` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `order` `Ring.toSemiring`	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `instMul` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instOne`	—	`coeff_mul_right_one_sub_of_lt_weightedOrder` `Finsupp.degree_eq_weight_one`
`coeff_mul_right_one_sub_of_lt_weightedOrder` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule` `weightedOrder` `Ring.toSemiring`	`LinearMap` `RingHom.id` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `instMul` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instOne`	—	`sub_mul` `one_mul` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `coeff_eq_zero_of_lt_weightedOrder` `lt_of_lt_of_le` `le_self_add` `le_weightedOrder_mul`
`coeff_of_lt_order` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `order`	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`coeff_eq_zero_of_lt_weightedOrder` `Finsupp.degree_eq_weight_one`
`coeff_weightedHomogeneousComponent` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `weightedHomogeneousComponent` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule`	—	—
`eq_zero_iff_forall_coeff_eq_zero_and` 📖	mathematical	—	`MvPowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff`	—	`eq_zero_iff_forall_coeff_zero`
`exists_coeff_ne_zero_and_order` 📖	mathematical	`ENat` `ENat.instNatCast` `ENat.toNat` `order`	`DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree`	—	`Finsupp.degree_eq_weight_one` `exists_coeff_ne_zero_and_weightedOrder`
`exists_coeff_ne_zero_and_weightedOrder` 📖	mathematical	`ENat` `ENat.instNatCast` `ENat.toNat` `weightedOrder`	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule`	—	`ne_zero_iff_weightedOrder_finite` `Nat.find_spec`
`homogeneousComponent_mul_of_le_order` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `order`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `homogeneousComponent` `instMul`	—	`weightedHomogeneousComponent_mul_of_le_weightedOrder`
`homogeneousComponent_of_lt_order_eq_zero` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `order`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `homogeneousComponent` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero`
`homogeneousComponent_of_order` 📖	—	`ENat` `ENat.instNatCast` `order`	—	—	`weightedHomogeneousComponent_of_weightedOrder`
`isHomogeneous_homogeneousComponent` 📖	mathematical	—	`IsHomogeneous` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `homogeneousComponent`	—	`isWeightedHomogeneous_weightedHomogeneousComponent`
`isHomogeneous_iff_eq_homogeneousComponent` 📖	mathematical	—	`IsHomogeneous` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `homogeneousComponent`	—	`isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent`
`isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent` 📖	mathematical	—	`IsWeightedHomogeneous` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent`	—	`ext` `coeff_weightedHomogeneousComponent` `IsWeightedHomogeneous.coeff_eq_zero` `isWeightedHomogeneous_weightedHomogeneousComponent`
`isWeightedHomogeneous_weightedHomogeneousComponent` 📖	mathematical	—	`IsWeightedHomogeneous` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent`	—	`not_imp_comm` `coeff_weightedHomogeneousComponent`
`le_order` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `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`	—	`le_weightedOrder` `Finsupp.degree_eq_weight_one`
`le_order_map` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `order` `DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `map`	—	`le_weightedOrder_map`
`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` `MvPowerSeries` `instMul`	—	`le_weightedOrder_mul`
`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` `MvPowerSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`le_weightedOrder_pow`
`le_order_pow_of_constantCoeff_eq_zero` 📖	mathematical	`DFunLike.coe` `RingHom` `MvPowerSeries` `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` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `order` `Finset.prod` `MvPowerSeries` `CommSemiring.toCommMonoid` `instCommSemiring`	—	`le_weightedOrder_prod`
`le_order_smul` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `order` `MvPowerSeries` `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_weightedOrder_smul`
`le_weightedOrder` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `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` `weightedOrder`	—	`top_le_iff` `weightedOrder_eq_top_iff` `ext` `ENat.coe_lt_top` `nat_le_weightedOrder` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`le_weightedOrder_map` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `weightedOrder` `DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `map`	—	`le_weightedOrder` `coeff_eq_zero_of_lt_weightedOrder` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`le_weightedOrder_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` `weightedOrder` `MvPowerSeries` `instMul`	—	`le_weightedOrder` `coeff_mul` `Finset.sum_eq_zero` `coeff_eq_zero_of_lt_weightedOrder` `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` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `Nat.cast_add`
`le_weightedOrder_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` `weightedOrder` `MvPowerSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`zero_nsmul` `pow_zero` `succ_nsmul` `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_weightedOrder_mul`
`le_weightedOrder_prod` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `weightedOrder` `Finset.prod` `MvPowerSeries` `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_weightedOrder_mul`
`le_weightedOrder_smul` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `weightedOrder` `MvPowerSeries` `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_weightedOrder` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `coeff_eq_zero_of_lt_weightedOrder` `MulZeroClass.mul_zero`
`min_order_le_add` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `SemilatticeInf.toMin` `order` `MvPowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring`	—	`min_weightedOrder_le_add`
`min_weightedOrder_le_add` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `SemilatticeInf.toMin` `weightedOrder` `MvPowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring`	—	`le_weightedOrder` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `coeff_eq_zero_of_lt_weightedOrder` `add_zero`
`nat_le_order` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `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`	—	`nat_le_weightedOrder` `Finsupp.degree_eq_weight_one`
`nat_le_weightedOrder` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `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` `weightedOrder`	—	`ENat.coe_toNat_eq_self` `ne_top_of_lt` `exists_coeff_ne_zero_and_weightedOrder` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`ne_zero_iff_exists_coeff_ne_zero_and_degree` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree`	—	`Finsupp.degree_eq_weight_one` `ne_zero_iff_exists_coeff_ne_zero_and_weight`
`ne_zero_iff_exists_coeff_ne_zero_and_weight` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule`	—	`ne_zero_iff_exists_coeff_ne_zero`
`ne_zero_iff_order_finite` 📖	mathematical	—	`ENat` `ENat.instNatCast` `ENat.toNat` `order`	—	`ne_zero_iff_weightedOrder_finite`
`ne_zero_iff_weightedOrder_finite` 📖	mathematical	—	`ENat` `ENat.instNatCast` `ENat.toNat` `weightedOrder`	—	—
`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` `MvPowerSeries` `instSemiring` `RingHom.instFunLike` `constantCoeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`coeff_of_lt_order` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `Nat.cast_zero` `Order.one_le_iff_pos` `IsOrderedRing.toZeroLEOneClass` `NeZero.one` `le_order` `Finsupp.degree_eq_zero_iff` `Nat.instCanonicallyOrderedAdd` `Nat.cast_lt_one` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid`
`order_add_of_order_ne` 📖	mathematical	—	`order` `MvPowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `ENat` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	—	`weightedOrder_add_of_weightedOrder_ne`
`order_eq_nat` 📖	mathematical	—	`order` `ENat` `ENat.instNatCast` `DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finsupp.degree_eq_weight_one` `weightedOrder_eq_nat`
`order_eq_top_iff` 📖	mathematical	—	`order` `Top.top` `ENat` `instTopENat` `MvPowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`weightedOrder_eq_top_iff`
`order_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `order` `ENat.instNatCast` `DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree`	—	`Finsupp.degree_eq_weight_one` `weightedOrder_le`
`order_monomial` 📖	mathematical	—	`order` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Top.top` `instTopENat` `ENat.instNatCast` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree`	—	`Finsupp.degree_eq_weight_one` `weightedOrder_monomial`
`order_monomial_of_ne_zero` 📖	mathematical	—	`order` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `ENat` `ENat.instNatCast` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree`	—	`Finsupp.degree_eq_weight_one` `weightedOrder_monomial_of_ne_zero`
`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` `MvPowerSeries` `instMul`	—	`le_order_mul`
`order_ne_zero_iff_constCoeff_eq_zero` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPowerSeries` `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` `MvPowerSeries` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `Ring.toAddCommGroup`	—	`weightedOrder_neg`
`order_toSubring` 📖	mathematical	`Subring` `SetLike.instMembership` `Subring.instSetLike` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `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` `MvPowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Top.top` `ENat` `instTopENat`	—	`weightedOrder_zero`
`weightedHomogeneousComponent_mul_of_le_weightedOrder` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `weightedOrder`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent` `instMul`	—	`ext` `coeff_weightedHomogeneousComponent` `Finset.sum_congr` `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` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `Finset.HasAntidiagonal.mem_antidiagonal` `ne_of_lt` `MulZeroClass.zero_mul` `coeff_eq_zero_of_lt_weightedOrder` `lt_of_lt_of_le` `ENat.coe_lt_coe` `MulZeroClass.mul_zero` `IsWeightedHomogeneous.coeff_eq_zero` `IsWeightedHomogeneous.mul` `isWeightedHomogeneous_weightedHomogeneousComponent`
`weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `weightedOrder`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `weightedHomogeneousComponent` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`ext` `coeff_weightedHomogeneousComponent` `coeff_zero` `coeff_eq_zero_of_lt_weightedOrder` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`weightedHomogeneousComponent_of_weightedOrder` 📖	—	`ENat` `ENat.instNatCast` `weightedOrder`	—	—	`exists_coeff_ne_zero_and_weightedOrder` `ENat.toNat_coe` `ext_iff`
`weightedOrder_add_of_weightedOrder_ne` 📖	mathematical	—	`weightedOrder` `MvPowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `ENat` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	—	`le_antisymm` `le_rfl` `le_of_lt` `add_comm` `inf_comm` `LE.le.lt_of_ne'` `le_of_not_gt` `min_weightedOrder_le_add`
`weightedOrder_eq_nat` 📖	mathematical	—	`weightedOrder` `ENat` `ENat.instNatCast` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule` `LinearMap` `RingHom.id` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff`	—	`exists_coeff_ne_zero_and_weightedOrder` `coeff_eq_zero_of_lt_weightedOrder` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `le_antisymm` `weightedOrder_le` `nat_le_weightedOrder`
`weightedOrder_eq_top_iff` 📖	mathematical	—	`weightedOrder` `Top.top` `ENat` `instTopENat` `MvPowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`not_iff_not` `ne_zero_iff_weightedOrder_finite` `ENat.coe_toNat_eq_self`
`weightedOrder_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `weightedOrder` `ENat.instNatCast` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule`	—	`weightedOrder.eq_1` `ne_zero_iff_exists_coeff_ne_zero_and_weight` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `le_rfl`
`weightedOrder_monomial` 📖	mathematical	—	`weightedOrder` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Top.top` `instTopENat` `ENat.instNatCast` `AddMonoidHom` `Finsupp` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule`	—	`weightedOrder_eq_top_iff` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `weightedOrder_eq_nat` `coeff_monomial_same` `coeff_monomial` `LT.lt.false`
`weightedOrder_monomial_of_ne_zero` 📖	mathematical	—	`weightedOrder` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `ENat` `ENat.instNatCast` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Nat.instSemiring` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.weight` `AddCommMonoid.toNatModule`	—	`weightedOrder_monomial`
`weightedOrder_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` `weightedOrder` `MvPowerSeries` `instMul`	—	`le_weightedOrder_mul`
`weightedOrder_neg` 📖	mathematical	—	`weightedOrder` `Ring.toSemiring` `MvPowerSeries` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `Ring.toAddCommGroup`	—	`neg_add_cancel` `weightedOrder_zero` `weightedOrder_add_of_weightedOrder_ne` `neg_zero`
`weightedOrder_one` 📖	mathematical	—	`weightedOrder` `MvPowerSeries` `instOne` `ENat` `instZeroENat`	—	`weightedOrder_monomial_of_ne_zero` `one_ne_zero` `NeZero.one`
`weightedOrder_toSubring` 📖	mathematical	`Subring` `SetLike.instMembership` `Subring.instSetLike` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff`	`weightedOrder` `Subring.toRing` `toSubring`	—	`eq_of_le_of_ge` `le_weightedOrder` `coeff_toSubring` `coeff_eq_zero_of_lt_weightedOrder` `Nat.cast_zero`
`weightedOrder_zero` 📖	mathematical	—	`weightedOrder` `MvPowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Top.top` `ENat` `instTopENat`	—	`weightedOrder.eq_1`

MvPowerSeries.IsHomogeneous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MvPowerSeries.IsHomogeneous`	`MvPowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPowerSeries.instSemiring`	—	`MvPowerSeries.IsWeightedHomogeneous.add`
`coeff_eq_zero` 📖	mathematical	`MvPowerSeries.IsHomogeneous`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `MvPowerSeries.coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`MvPowerSeries.IsWeightedHomogeneous.coeff_eq_zero` `Finsupp.degree_eq_weight_one`
`mul` 📖	mathematical	`MvPowerSeries.IsHomogeneous`	`MvPowerSeries` `MvPowerSeries.instMul`	—	`MvPowerSeries.IsWeightedHomogeneous.mul`

MvPowerSeries.IsWeightedHomogeneous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MvPowerSeries.IsWeightedHomogeneous`	`MvPowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPowerSeries.instSemiring`	—	`not_imp_comm` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `coeff_eq_zero` `add_zero`
`coeff_eq_zero` 📖	mathematical	`MvPowerSeries.IsWeightedHomogeneous`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `MvPowerSeries.coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`mul` 📖	mathematical	`MvPowerSeries.IsWeightedHomogeneous`	`MvPowerSeries` `MvPowerSeries.instMul`	—	`not_imp_comm` `MvPowerSeries.coeff_mul` `Finset.sum_eq_zero` `not_and_or` `Finset.HasAntidiagonal.mem_antidiagonal` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `coeff_eq_zero` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`

---

← Back to Index