TrailingDegree

📁 Source: Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean

Statistics

Metric	Count
Definitions `TrailingMonic`, `decidable`, `natTrailingDegree`, `nextCoeffUp`, `trailingCoeff`, `trailingDegree`	6
Theorems `eq_X_pow_iff_natDegree_le_natTrailingDegree`, `eq_X_pow_iff_natTrailingDegree_eq_natDegree`, `def`, `trailingCoeff`, `coeff_eq_zero_of_lt_natTrailingDegree`, `coeff_eq_zero_of_lt_trailingDegree`, `coeff_mul_natTrailingDegree_add_natTrailingDegree`, `coeff_natTrailingDegree_eq_zero`, `coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt`, `coeff_natTrailingDegree_ne_zero`, `coeff_natTrailingDegree_pred_eq_zero`, `le_natTrailingDegree`, `le_natTrailingDegree_mul`, `le_trailingDegree_C`, `le_trailingDegree_C_mul_X_pow`, `le_trailingDegree_X`, `le_trailingDegree_X_pow`, `le_trailingDegree_monomial`, `le_trailingDegree_mul`, `natTrailingDegree_C`, `natTrailingDegree_X`, `natTrailingDegree_X_le`, `natTrailingDegree_X_pow`, `natTrailingDegree_eq_of_trailingDegree_eq`, `natTrailingDegree_eq_of_trailingDegree_eq_some`, `natTrailingDegree_eq_support_min'`, `natTrailingDegree_eq_zero`, `natTrailingDegree_eq_zero_of_constantCoeff_ne_zero`, `natTrailingDegree_intCast`, `natTrailingDegree_le_natDegree`, `natTrailingDegree_le_natTrailingDegree`, `natTrailingDegree_le_of_mem_supp`, `natTrailingDegree_le_of_ne_zero`, `natTrailingDegree_le_of_trailingDegree_le`, `natTrailingDegree_le_trailingDegree`, `natTrailingDegree_mem_support_of_nonzero`, `natTrailingDegree_monomial`, `natTrailingDegree_monomial_le`, `natTrailingDegree_mul`, `natTrailingDegree_mul'`, `natTrailingDegree_mul_X_pow`, `natTrailingDegree_natCast`, `natTrailingDegree_ne_zero`, `natTrailingDegree_neg`, `natTrailingDegree_one`, `natTrailingDegree_zero`, `ne_zero_of_trailingDegree_lt`, `nextCoeffUp_C_eq_zero`, `nextCoeffUp_of_constantCoeff_eq_zero`, `nextCoeffUp_zero`, `trailingCoeff_eq_coeff_zero`, `trailingCoeff_eq_zero`, `trailingCoeff_nonzero_iff_nonzero`, `trailingCoeff_zero`, `trailingDegree_C`, `trailingDegree_C_mul_X_pow`, `trailingDegree_X`, `trailingDegree_X_pow`, `trailingDegree_eq_iff_natTrailingDegree_eq`, `trailingDegree_eq_iff_natTrailingDegree_eq_of_pos`, `trailingDegree_eq_natTrailingDegree`, `trailingDegree_eq_top`, `trailingDegree_eq_zero`, `trailingDegree_le_of_ne_zero`, `trailingDegree_le_trailingDegree`, `trailingDegree_lt_wf`, `trailingDegree_monomial`, `trailingDegree_mul'`, `trailingDegree_ne_of_natTrailingDegree_ne`, `trailingDegree_ne_zero`, `trailingDegree_neg`, `trailingDegree_one`, `trailingDegree_one_le`, `trailingDegree_zero`	74
Total	80

Polynomial

Definitions

Name	Category	Theorems
`TrailingMonic` 📖	MathDef	1 math math: `TrailingMonic.def`
`natTrailingDegree` 📖	CompOp	62 math math: `coeff_natTrailingDegree_eq_zero`, `LinearMap.isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank`, `rootMultiplicity_eq_natTrailingDegree`, `coeff_mul_natTrailingDegree_add_natTrailingDegree`, `rootMultiplicity_eq_natTrailingDegree'`, `natTrailingDegree_le_of_trailingDegree_le`, `LieAlgebra.finrank_engel`, `LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank`, `LinearMap.charpoly_nilpotent_tfae`, `LinearMap.nilRankAux_basis_indep`, `LieAlgebra.rank_le_natTrailingDegree_charpoly_ad`, `Monic.eq_X_pow_iff_natDegree_le_natTrailingDegree`, `natTrailingDegree_C`, `LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree`, `natTrailingDegree_mul_X_pow`, `trinomial_natTrailingDegree`, `natTrailingDegree_monomial`, `nextCoeffUp_of_constantCoeff_eq_zero`, `natTrailingDegree_natCast`, `Monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree`, `natTrailingDegree_mul_mirror`, `natTrailingDegree_eq_zero`, `LieModule.rank_eq_natTrailingDegree`, `natTrailingDegree_one`, `natTrailingDegree_X_le`, `coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt`, `natTrailingDegree_eq_zero_of_constantCoeff_ne_zero`, `natTrailingDegree_le_trailingDegree`, `natTrailingDegree_le_natTrailingDegree`, `natTrailingDegree_X`, `LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank`, `LinearMap.finrank_maxGenEigenspace`, `natTrailingDegree_eq_support_min'`, `natTrailingDegree_le_natDegree`, `natTrailingDegree_neg`, `natTrailingDegree_mem_support_of_nonzero`, `trailingDegree_eq_iff_natTrailingDegree_eq`, `LieAlgebra.rank_eq_natTrailingDegree`, `natTrailingDegree_X_pow`, `LinearMap.finrank_maxGenEigenspace_zero_eq`, `natTrailingDegree_eq_of_trailingDegree_eq`, `natTrailingDegree_mul`, `le_natTrailingDegree`, `coeff_mirror`, `natTrailingDegree_monomial_le`, `mirror_natTrailingDegree`, `natTrailingDegree_reverse`, `isUnitTrinomial_iff'`, `reverse_natDegree`, `natTrailingDegree_zero`, `LinearMap.nilRank_le_natTrailingDegree_charpoly`, `coeff_mul_mirror`, `natTrailingDegree_le_of_mem_supp`, `trailingDegree_eq_natTrailingDegree`, `le_natTrailingDegree_mul`, `natTrailingDegree_intCast`, `natDegree_eq_reverse_natDegree_add_natTrailingDegree`, `natTrailingDegree_mul'`, `natTrailingDegree_eq_of_trailingDegree_eq_some`, `natTrailingDegree_le_of_ne_zero`, `LieModule.rank_le_natTrailingDegree_charpoly_ad`, `trailingDegree_eq_iff_natTrailingDegree_eq_of_pos`
`nextCoeffUp` 📖	CompOp	3 math math: `nextCoeffUp_C_eq_zero`, `nextCoeffUp_zero`, `nextCoeffUp_of_constantCoeff_eq_zero`
`trailingCoeff` 📖	CompOp	14 math math: `coeff_mul_natTrailingDegree_add_natTrailingDegree`, `mirror_trailingCoeff`, `eval_divByMonic_eq_trailingCoeff_comp`, `reverse_trailingCoeff`, `trinomial_trailingCoeff`, `mirror_leadingCoeff`, `TrailingMonic.trailingCoeff`, `trailingCoeff_zero`, `trailingCoeff_eq_coeff_zero`, `TrailingMonic.def`, `reverse_leadingCoeff`, `IsUnitTrinomial.trailingCoeff_isUnit`, `trailingCoeff_eq_zero`, `trailingCoeff_mul`
`trailingDegree` 📖	CompOp	26 math math: `le_trailingDegree_C`, `trailingDegree_eq_zero`, `le_trailingDegree_monomial`, `trailingDegree_le_trailingDegree`, `trailingDegree_C_mul_X_pow`, `trailingDegree_zero`, `le_trailingDegree_mul`, `trailingDegree_le_of_ne_zero`, `le_trailingDegree_C_mul_X_pow`, `trailingDegree_C`, `natTrailingDegree_le_trailingDegree`, `trailingDegree_lt_wf`, `trailingDegree_one`, `trailingDegree_eq_iff_natTrailingDegree_eq`, `trailingDegree_eq_natTrailingDegree`, `trailingDegree_mul'`, `le_trailingDegree_X_pow`, `trailingDegree_neg`, `trailingDegree_monomial`, `trailingDegree_eq_top`, `trailingDegree_one_le`, `le_trailingDegree_X`, `trailingDegree_X_pow`, `trailingDegree_X`, `trailingDegree_mul`, `trailingDegree_eq_iff_natTrailingDegree_eq_of_pos`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_eq_zero_of_lt_natTrailingDegree` 📖	mathematical	`natTrailingDegree`	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`coeff_eq_zero_of_lt_trailingDegree` `trailingDegree_zero` `WithTop.coe_lt_top` `trailingDegree_eq_natTrailingDegree` `WithTop.coe_lt_coe`
`coeff_eq_zero_of_lt_trailingDegree` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `trailingDegree`	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`trailingDegree_le_of_ne_zero` `not_le_of_gt`
`coeff_mul_natTrailingDegree_add_natTrailingDegree` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `natTrailingDegree` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `trailingCoeff`	—	`coeff_mul` `Finset.sum_eq_single` `coeff_eq_zero_of_lt_natTrailingDegree` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `add_eq_add_iff_eq_and_eq` `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_natTrailingDegree_eq_zero` 📖	mathematical	—	`coeff` `natTrailingDegree` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial` `instZero`	—	`Finset.min_mem_image_coe` `support_nonempty` `trailingDegree_eq_iff_natTrailingDegree_eq`
`coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `trailingDegree`	`coeff` `natTrailingDegree` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`coeff_eq_zero_of_lt_trailingDegree` `LE.le.trans_lt` `natTrailingDegree_le_trailingDegree`
`coeff_natTrailingDegree_ne_zero` 📖	—	—	—	—	`Iff.not` `coeff_natTrailingDegree_eq_zero`
`coeff_natTrailingDegree_pred_eq_zero` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instZeroENat` `ENat.instNatCast` `natTrailingDegree`	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`coeff_eq_zero_of_lt_natTrailingDegree` `WithTop.coe_pos`
`le_natTrailingDegree` 📖	mathematical	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`natTrailingDegree`	—	`nonempty_support_iff` `natTrailingDegree_eq_support_min'` `Finset.le_min'` `not_lt` `mem_support_iff`
`le_natTrailingDegree_mul` 📖	mathematical	—	`natTrailingDegree` `Polynomial` `instMul`	—	`MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `WithTop.coe_le_coe` `WithTop.coe_add` `Nat.cast_withTop` `trailingDegree_eq_natTrailingDegree` `le_trailingDegree_mul`
`le_trailingDegree_C` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instZeroENat` `trailingDegree` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`le_trailingDegree_monomial`
`le_trailingDegree_C_mul_X_pow` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `trailingDegree` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`C_mul_X_pow_eq_monomial` `le_trailingDegree_monomial`
`le_trailingDegree_X` 📖	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` `trailingDegree` `X`	—	`le_trailingDegree_monomial`
`le_trailingDegree_X_pow` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `trailingDegree` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`one_mul` `le_trailingDegree_C_mul_X_pow`
`le_trailingDegree_monomial` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `trailingDegree` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	`monomial_zero_right` `Eq.ge` `trailingDegree_monomial`
`le_trailingDegree_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` `trailingDegree` `Polynomial` `instMul`	—	`Finset.le_min` `Finset.exists_ne_zero_of_sum_ne_zero` `coeff_mul` `mem_support_iff` `LE.le.trans_eq` `add_le_add` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithTop.addRightMono` `covariant_swap_add_of_covariant_add` `Finset.min_le` `left_ne_zero_of_mul` `right_ne_zero_of_mul` `WithTop.coe_add` `WithTop.coe_eq_coe` `Finset.HasAntidiagonal.mem_antidiagonal`
`natTrailingDegree_C` 📖	mathematical	—	`natTrailingDegree` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`nonpos_iff_eq_zero` `Nat.instCanonicallyOrderedAdd` `natTrailingDegree_monomial_le`
`natTrailingDegree_X` 📖	mathematical	—	`natTrailingDegree` `X`	—	`natTrailingDegree_monomial` `one_ne_zero` `NeZero.one`
`natTrailingDegree_X_le` 📖	mathematical	—	`natTrailingDegree` `X`	—	`natTrailingDegree_monomial_le`
`natTrailingDegree_X_pow` 📖	mathematical	—	`natTrailingDegree` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`X_pow_eq_monomial` `natTrailingDegree_monomial` `one_ne_zero` `NeZero.one`
`natTrailingDegree_eq_of_trailingDegree_eq` 📖	mathematical	`trailingDegree`	`natTrailingDegree`	—	—
`natTrailingDegree_eq_of_trailingDegree_eq_some` 📖	mathematical	`trailingDegree` `ENat` `ENat.instNatCast`	`natTrailingDegree`	—	—
`natTrailingDegree_eq_support_min'` 📖	mathematical	—	`natTrailingDegree` `Finset.min'` `Nat.instLinearOrder` `support` `Finset.Nonempty` `Polynomial` `instZero` `nonempty_support_iff`	—	`nonempty_support_iff` `natTrailingDegree.eq_1` `trailingDegree.eq_1` `Finset.coe_min'` `ENat.some_eq_coe` `ENat.toNat_coe`
`natTrailingDegree_eq_zero` 📖	mathematical	—	`natTrailingDegree` `Polynomial` `instZero`	—	—
`natTrailingDegree_eq_zero_of_constantCoeff_ne_zero` 📖	mathematical	—	`natTrailingDegree`	—	`le_antisymm` `natTrailingDegree_le_of_ne_zero` `zero_le'`
`natTrailingDegree_intCast` 📖	mathematical	—	`natTrailingDegree` `Ring.toSemiring` `Polynomial` `instIntCast`	—	`natTrailingDegree_C`
`natTrailingDegree_le_natDegree` 📖	mathematical	—	`natTrailingDegree` `natDegree`	—	`natDegree_zero` `natTrailingDegree_zero` `le_refl` `le_natDegree_of_ne_zero` `trailingCoeff_eq_zero`
`natTrailingDegree_le_natTrailingDegree` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `trailingDegree`	`natTrailingDegree`	—	`ENat.toNat_le_toNat`
`natTrailingDegree_le_of_mem_supp` 📖	mathematical	`Finset` `Finset.instMembership` `support`	`natTrailingDegree`	—	`natTrailingDegree_le_of_ne_zero` `mem_support_iff`
`natTrailingDegree_le_of_ne_zero` 📖	mathematical	—	`natTrailingDegree`	—	`ENat.toNat_le_of_le_coe` `trailingDegree_le_of_ne_zero`
`natTrailingDegree_le_of_trailingDegree_le` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `trailingDegree`	`natTrailingDegree`	—	`Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `trailingDegree_eq_natTrailingDegree`
`natTrailingDegree_le_trailingDegree` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `natTrailingDegree` `trailingDegree`	—	`ENat.coe_toNat_le_self`
`natTrailingDegree_mem_support_of_nonzero` 📖	mathematical	—	`Finset` `Finset.instMembership` `support` `natTrailingDegree`	—	`mem_support_iff` `trailingCoeff_nonzero_iff_nonzero`
`natTrailingDegree_monomial` 📖	mathematical	—	`natTrailingDegree` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	`natTrailingDegree.eq_1` `trailingDegree_monomial`
`natTrailingDegree_monomial_le` 📖	mathematical	—	`natTrailingDegree` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	`monomial_zero_right` `Nat.instCanonicallyOrderedAdd` `Eq.le` `natTrailingDegree_monomial`
`natTrailingDegree_mul` 📖	mathematical	—	`natTrailingDegree` `Polynomial` `instMul`	—	`natTrailingDegree_mul'` `mul_ne_zero` `trailingCoeff_eq_zero`
`natTrailingDegree_mul'` 📖	mathematical	—	`natTrailingDegree` `Polynomial` `instMul`	—	`trailingCoeff_zero` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `natTrailingDegree_eq_of_trailingDegree_eq_some` `trailingDegree_mul'` `Nat.cast_withTop` `WithTop.coe_add` `trailingDegree_eq_natTrailingDegree`
`natTrailingDegree_mul_X_pow` 📖	mathematical	—	`natTrailingDegree` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`le_antisymm` `natTrailingDegree_le_of_ne_zero` `trailingCoeff_eq_zero` `trailingCoeff.eq_1` `coeff_mul_X_pow` `nonempty_support_iff` `mul_X_pow_eq_zero` `natTrailingDegree_eq_support_min'` `Finset.le_min'_iff` `by_contra` `coeff_mul_X_pow'` `mem_support_iff` `le_tsub_iff_right` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`
`natTrailingDegree_natCast` 📖	mathematical	—	`natTrailingDegree` `Polynomial` `instNatCast`	—	`natTrailingDegree_C`
`natTrailingDegree_ne_zero` 📖	mathematical	—	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Iff.not` `natTrailingDegree_eq_zero` `not_ne_iff`
`natTrailingDegree_neg` 📖	mathematical	—	`natTrailingDegree` `Ring.toSemiring` `Polynomial` `instNeg`	—	`trailingDegree_neg`
`natTrailingDegree_one` 📖	mathematical	—	`natTrailingDegree` `Polynomial` `instOne`	—	`natTrailingDegree_C`
`natTrailingDegree_zero` 📖	mathematical	—	`natTrailingDegree` `Polynomial` `instZero`	—	—
`ne_zero_of_trailingDegree_lt` 📖	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `trailingDegree`	—	—	`LT.lt.not_ge`
`nextCoeffUp_C_eq_zero` 📖	mathematical	—	`nextCoeffUp` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`nextCoeffUp.eq_1` `natTrailingDegree_C`
`nextCoeffUp_of_constantCoeff_eq_zero` 📖	mathematical	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`nextCoeffUp` `natTrailingDegree`	—	`eq_or_ne` `nextCoeffUp_zero` `zero_add` `nextCoeffUp.eq_1` `natTrailingDegree_ne_zero`
`nextCoeffUp_zero` 📖	mathematical	—	`nextCoeffUp` `Polynomial` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`trailingCoeff_eq_coeff_zero` 📖	mathematical	—	`trailingCoeff` `coeff`	—	`trailingCoeff.eq_1` `natTrailingDegree_eq_zero`
`trailingCoeff_eq_zero` 📖	mathematical	—	`trailingCoeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial` `instZero`	—	`by_contradiction` `mem_support_iff` `Finset.mem_of_min` `trailingDegree_eq_natTrailingDegree` `leadingCoeff_zero`
`trailingCoeff_nonzero_iff_nonzero` 📖	—	—	—	—	`trailingCoeff_eq_zero`
`trailingCoeff_zero` 📖	mathematical	—	`trailingCoeff` `Polynomial` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`trailingDegree_C` 📖	mathematical	—	`trailingDegree` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `ENat` `instZeroENat`	—	`trailingDegree_monomial`
`trailingDegree_C_mul_X_pow` 📖	mathematical	—	`trailingDegree` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `ENat` `ENat.instNatCast`	—	`C_mul_X_pow_eq_monomial` `trailingDegree_monomial`
`trailingDegree_X` 📖	mathematical	—	`trailingDegree` `X` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`trailingDegree_monomial` `one_ne_zero` `NeZero.one`
`trailingDegree_X_pow` 📖	mathematical	—	`trailingDegree` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `ENat` `ENat.instNatCast`	—	`X_pow_eq_monomial` `trailingDegree_monomial` `one_ne_zero` `NeZero.one`
`trailingDegree_eq_iff_natTrailingDegree_eq` 📖	mathematical	—	`trailingDegree` `ENat` `ENat.instNatCast` `natTrailingDegree`	—	`trailingDegree_eq_natTrailingDegree`
`trailingDegree_eq_iff_natTrailingDegree_eq_of_pos` 📖	mathematical	—	`trailingDegree` `ENat` `ENat.instNatCast` `natTrailingDegree`	—	`natTrailingDegree.eq_1` `ENat.toNat_eq_iff`
`trailingDegree_eq_natTrailingDegree` 📖	mathematical	—	`trailingDegree` `ENat` `ENat.instNatCast` `natTrailingDegree`	—	`ENat.coe_toNat` `trailingDegree_eq_top`
`trailingDegree_eq_top` 📖	mathematical	—	`trailingDegree` `Top.top` `ENat` `instTopENat` `Polynomial` `instZero`	—	`support_eq_empty` `Finset.min_eq_top`
`trailingDegree_eq_zero` 📖	mathematical	—	`trailingDegree` `ENat` `instZeroENat`	—	`Finset.min_eq_bot` `mem_support_iff`
`trailingDegree_le_of_ne_zero` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `trailingDegree` `ENat.instNatCast`	—	`Finset.min_le` `mem_support_iff`
`trailingDegree_le_trailingDegree` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `trailingDegree`	—	`LE.le.trans` `trailingDegree_le_of_ne_zero` `natTrailingDegree_le_trailingDegree`
`trailingDegree_lt_wf` 📖	mathematical	—	`Polynomial` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `trailingDegree`	—	`wellFounded_lt`
`trailingDegree_monomial` 📖	mathematical	—	`trailingDegree` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `ENat` `ENat.instNatCast`	—	`trailingDegree.eq_1` `support_monomial` `Finset.min_singleton`
`trailingDegree_mul'` 📖	mathematical	—	`trailingDegree` `Polynomial` `instMul` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`trailingCoeff_zero` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `le_antisymm` `trailingDegree_eq_natTrailingDegree` `ENat.coe_add` `trailingDegree_le_of_ne_zero` `coeff_mul_natTrailingDegree_add_natTrailingDegree` `le_trailingDegree_mul`
`trailingDegree_ne_of_natTrailingDegree_ne` 📖	—	—	—	—	`natTrailingDegree.eq_1` `ENat.toNat_coe`
`trailingDegree_ne_zero` 📖	mathematical	—	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Iff.not_left` `trailingDegree_eq_zero`
`trailingDegree_neg` 📖	mathematical	—	`trailingDegree` `Ring.toSemiring` `Polynomial` `instNeg`	—	`support_neg`
`trailingDegree_one` 📖	mathematical	—	`trailingDegree` `Polynomial` `instOne` `ENat` `instZeroENat`	—	`trailingDegree_C` `one_ne_zero` `NeZero.one`
`trailingDegree_one_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instZeroENat` `trailingDegree` `Polynomial` `instOne`	—	`C_1` `le_trailingDegree_C`
`trailingDegree_zero` 📖	mathematical	—	`trailingDegree` `Polynomial` `instZero` `Top.top` `ENat` `instTopENat`	—	—

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_X_pow_iff_natDegree_le_natTrailingDegree` 📖	mathematical	`Polynomial.Monic`	`Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.natDegree` `Polynomial.natTrailingDegree`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Polynomial.natDegree_of_subsingleton` `Nat.instCanonicallyOrderedAdd` `Polynomial.natTrailingDegree_X_pow` `le_refl` `Polynomial.ext` `Polynomial.coeff_X_pow` `lt_trichotomy` `LT.lt.ne` `Polynomial.coeff_eq_zero_of_lt_natTrailingDegree` `LT.lt.trans_le` `leadingCoeff` `LT.lt.ne'` `Polynomial.coeff_eq_zero_of_natDegree_lt`
`eq_X_pow_iff_natTrailingDegree_eq_natDegree` 📖	mathematical	`Polynomial.Monic`	`Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.natDegree` `Polynomial.natTrailingDegree`	—	`eq_X_pow_iff_natDegree_le_natTrailingDegree` `LE.le.ge_iff_eq` `Polynomial.natTrailingDegree_le_natDegree`

Polynomial.TrailingMonic

Definitions

Name	Category	Theorems
`decidable` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`def` 📖	mathematical	—	`Polynomial.TrailingMonic` `Polynomial.trailingCoeff` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	—
`trailingCoeff` 📖	mathematical	`Polynomial.TrailingMonic`	`Polynomial.trailingCoeff` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	—

---

← Back to Index