Reverse

📁 Source: Mathlib/Algebra/Polynomial/Reverse.lean

Statistics

Metric	Count
Definitions `reflect`, `revAt`, `revAtFun`, `reverse`	4
Theorems `coeff_one_reverse`, `coeff_reflect`, `coeff_reverse`, `coeff_zero_reverse`, `eval₂_reflect_eq_zero_iff`, `eval₂_reflect_mul_pow`, `eval₂_reverse_eq_zero_iff`, `eval₂_reverse_mul_pow`, `natDegree_eq_reverse_natDegree_add_natTrailingDegree`, `natDegree_reflect_le`, `natTrailingDegree_reverse`, `reflect_C`, `reflect_C_mul`, `reflect_C_mul_X_pow`, `reflect_add`, `reflect_eq_zero_iff`, `reflect_map`, `reflect_monomial`, `reflect_mul`, `reflect_mul_induction`, `reflect_neg`, `reflect_one`, `reflect_one_X`, `reflect_reflect`, `reflect_sub`, `reflect_support`, `reflect_zero`, `revAtFun_eq`, `revAtFun_inj`, `revAtFun_invol`, `revAt_add`, `revAt_eq_self_of_lt`, `revAt_invol`, `revAt_le`, `revAt_zero`, `reverse_C`, `reverse_C_add`, `reverse_X_mul`, `reverse_X_pow_mul`, `reverse_add_C`, `reverse_eq_zero`, `reverse_leadingCoeff`, `reverse_mul`, `reverse_mul_X`, `reverse_mul_X_pow`, `reverse_mul_of_domain`, `reverse_natDegree`, `reverse_natDegree_le`, `reverse_neg`, `reverse_trailingCoeff`, `reverse_zero`, `trailingCoeff_mul`	52
Total	56

Polynomial

Definitions

Name	Category	Theorems
`reflect` 📖	CompOp	21 math math: `reflect_sub`, `eval₂_reflect_eq_zero_iff`, `reflect_map`, `reflect_add`, `eval₂_reflect_mul_pow`, `reflect_one`, `reflect_monomial`, `reflect_one_X`, `natDegree_reflect_le`, `reflect_support`, `coeff_reflect`, `reflect_zero`, `reflect_reflect`, `reflect_mul`, `reflect_neg`, `reflect_C_mul_X_pow`, `reflect_C`, `reflect_C_mul`, `isNilpotent_reflect_iff`, `reflect_eq_zero_iff`, `reflect_mul_induction`
`revAt` 📖	CompOp	12 math math: `revAt_zero`, `revAt_eq_self_of_lt`, `reflect_monomial`, `reflect_support`, `coeff_reflect`, `revAt_le`, `reflect_C_mul_X_pow`, `revAtFun_eq`, `coeff_mirror`, `revAt_add`, `revAt_invol`, `coeff_reverse`
`revAtFun` 📖	CompOp	3 math math: `revAtFun_invol`, `revAtFun_inj`, `revAtFun_eq`
`reverse` 📖	CompOp	26 math math: `reverse_mul_X_pow`, `reverse_eq_zero`, `reverse_trailingCoeff`, `reverse_mul_of_domain`, `Matrix.reverse_charpoly`, `reverse_X_pow_mul`, `reverse_mul_X`, `reverse_natDegree_le`, `reverse_X_mul`, `reverse_add_C`, `reverse_mul`, `coeff_one_reverse`, `reverse_neg`, `reverse_C`, `reverse_leadingCoeff`, `reverse_zero`, `natTrailingDegree_reverse`, `eval₂_reverse_mul_pow`, `reverse_natDegree`, `coeff_zero_reverse`, `coeff_reverse`, `reverse_C_add`, `LaurentPolynomial.toLaurent_reverse`, `isNilpotent_reverse_iff`, `natDegree_eq_reverse_natDegree_add_natTrailingDegree`, `eval₂_reverse_eq_zero_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_one_reverse` 📖	mathematical	—	`coeff` `reverse` `nextCoeff`	—	`coeff_reverse` `nextCoeff.eq_1` `coeff_eq_zero_of_natDegree_lt` `Nat.instZeroLEOneClass` `Nat.instCanonicallyOrderedAdd` `zero_tsub` `Nat.instOrderedSub` `revAt_le` `pos_iff_ne_zero`
`coeff_reflect` 📖	mathematical	—	`coeff` `reflect` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `revAt`	—	`revAt_invol` `Finsupp.embDomain_apply_self`
`coeff_reverse` 📖	mathematical	—	`coeff` `reverse` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `revAt` `natDegree`	—	`reverse.eq_1` `coeff_reflect`
`coeff_zero_reverse` 📖	mathematical	—	`coeff` `reverse` `leadingCoeff`	—	`coeff_reverse` `revAt_le` `zero_le` `Nat.instCanonicallyOrderedAdd` `tsub_zero` `Nat.instOrderedSub` `leadingCoeff.eq_1`
`eval₂_reflect_eq_zero_iff` 📖	mathematical	`natDegree`	`eval₂` `CommSemiring.toSemiring` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `reflect` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`eval₂_reflect_mul_pow` `MulZeroClass.zero_mul` `mul_one` `one_pow` `mul_invOf_self` `mul_pow` `mul_assoc`
`eval₂_reflect_mul_pow` 📖	mathematical	`natDegree`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `eval₂` `Invertible.invOf` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `reflect` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`induction_with_natDegree_le` `eval₂_zero` `MulZeroClass.zero_mul` `reflect_C_mul_X_pow` `revAt_le` `eval₂_mul` `eval₂_C` `eval₂_X_pow` `pow_add` `mul_assoc` `mul_pow` `invOf_mul_self` `one_pow` `mul_one` `reflect_add` `eval₂_add` `add_mul` `Distrib.rightDistribClass`
`eval₂_reverse_eq_zero_iff` 📖	mathematical	—	`eval₂` `CommSemiring.toSemiring` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `reverse` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`eval₂_reflect_eq_zero_iff` `le_rfl`
`eval₂_reverse_mul_pow` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `eval₂` `Invertible.invOf` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `reverse` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `natDegree`	—	`eval₂_reflect_mul_pow` `le_rfl`
`natDegree_eq_reverse_natDegree_add_natTrailingDegree` 📖	mathematical	—	`natDegree` `reverse` `natTrailingDegree`	—	`reverse_zero` `natDegree_zero` `natTrailingDegree_zero` `le_antisymm` `tsub_le_iff_right` `Nat.instOrderedSub` `le_natDegree_of_ne_zero` `reverse.eq_1` `coeff_reflect` `revAt_le` `natTrailingDegree_le_natDegree` `revAt_invol` `trailingCoeff_nonzero_iff_nonzero` `le_tsub_iff_left` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `reverse_natDegree_le` `natTrailingDegree_le_of_ne_zero` `leadingCoeff_eq_zero` `reverse_eq_zero` `coeff_reverse` `leadingCoeff.eq_1`
`natDegree_reflect_le` 📖	mathematical	—	`natDegree` `reflect`	—	`coeff_reflect` `coeff_eq_zero_of_natDegree_lt`
`natTrailingDegree_reverse` 📖	mathematical	—	`natTrailingDegree` `reverse`	—	`natTrailingDegree_eq_zero` `reverse_eq_zero` `coeff_zero_reverse` `leadingCoeff_ne_zero` `eq_or_ne`
`reflect_C` 📖	mathematical	—	`reflect` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`mul_one` `pow_zero` `reflect_C_mul_X_pow` `revAt_zero`
`reflect_C_mul` 📖	mathematical	—	`reflect` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`ext` `coeff_reflect` `coeff_C_mul`
`reflect_C_mul_X_pow` 📖	mathematical	—	`reflect` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `Function.Embedding` `Function.instFunLikeEmbedding` `revAt`	—	`ext`
`reflect_add` 📖	mathematical	—	`reflect` `Polynomial` `instAdd`	—	`ext` `coeff_reflect` `coeff_add`
`reflect_eq_zero_iff` 📖	mathematical	—	`reflect` `Polynomial` `instZero`	—	`ofFinsupp_eq_zero` `reflect.eq_1` `Finsupp.embDomain_eq_zero`
`reflect_map` 📖	mathematical	—	`reflect` `map`	—	`ext` `coeff_reflect` `coeff_map`
`reflect_monomial` 📖	mathematical	—	`reflect` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `revAt`	—	`one_mul` `C_1` `reflect_C_mul_X_pow`
`reflect_mul` 📖	mathematical	`natDegree`	`reflect` `Polynomial` `instMul`	—	`reflect_mul_induction`
`reflect_mul_induction` 📖	mathematical	`Finset.card` `support` `natDegree`	`reflect` `Polynomial` `instMul`	—	`C_mul_X_pow_eq_self` `mul_assoc` `X_pow_mul` `pow_add` `reflect_C_mul` `reflect_monomial` `add_comm` `revAt_add` `reflect_zero` `MulZeroClass.mul_zero` `eraseLead_add_C_mul_X_pow` `mul_add` `Distrib.leftDistribClass` `reflect_add` `lt_of_lt_of_le` `eraseLead_support_card_lt` `le_trans` `eraseLead_natDegree_le_aux` `le_add_left` `Nat.instCanonicallyOrderedAdd` `card_support_C_mul_X_pow_le_one` `natDegree_C_mul_X_pow_le` `MulZeroClass.zero_mul` `add_mul` `Distrib.rightDistribClass`
`reflect_neg` 📖	mathematical	—	`reflect` `Ring.toSemiring` `Polynomial` `instNeg`	—	`neg_eq_neg_one_mul` `C_1` `C_neg` `reflect_C_mul`
`reflect_one` 📖	mathematical	—	`reflect` `Polynomial` `instOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`RingHom.map_one` `reflect_C` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul`
`reflect_one_X` 📖	mathematical	—	`reflect` `X` `Polynomial` `instOne`	—	`pow_one` `revAt_le` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `reflect_monomial`
`reflect_reflect` 📖	mathematical	—	`reflect`	—	`ext` `coeff_reflect` `revAt_invol`
`reflect_sub` 📖	mathematical	—	`reflect` `Ring.toSemiring` `Polynomial` `instSub`	—	`sub_eq_add_neg` `reflect_add` `reflect_neg`
`reflect_support` 📖	mathematical	—	`support` `reflect` `Finset.image` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `revAt`	—	`Finset.ext` `support_ofFinsupp`
`reflect_zero` 📖	mathematical	—	`reflect` `Polynomial` `instZero`	—	—
`revAtFun_eq` 📖	mathematical	—	`revAtFun` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `revAt`	—	—
`revAtFun_inj` 📖	mathematical	—	`revAtFun`	—	`revAtFun_invol`
`revAtFun_invol` 📖	mathematical	—	`revAtFun`	—	—
`revAt_add` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `revAt`	—	`revAt_le` `le_add_right` `Nat.instCanonicallyOrderedAdd` `Eq.le` `add_assoc` `add_left_comm` `add_tsub_cancel_left` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`revAt_eq_self_of_lt` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `revAt`	—	—
`revAt_invol` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `revAt`	—	`revAtFun_invol`
`revAt_le` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `revAt`	—	—
`revAt_zero` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `revAt`	—	`revAt_le` `Nat.instCanonicallyOrderedAdd` `tsub_zero` `Nat.instOrderedSub`
`reverse_C` 📖	mathematical	—	`reverse` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`natDegree_C` `reflect_C` `pow_zero` `mul_one`
`reverse_C_add` 📖	mathematical	—	`reverse` `Polynomial` `instAdd` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `natDegree`	—	`add_comm` `reverse_add_C`
`reverse_X_mul` 📖	mathematical	—	`reverse` `Polynomial` `instMul` `X`	—	`commute_X` `reverse_mul_X`
`reverse_X_pow_mul` 📖	mathematical	—	`reverse` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`commute_X_pow` `reverse_mul_X_pow`
`reverse_add_C` 📖	mathematical	—	`reverse` `Polynomial` `instAdd` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `natDegree`	—	`natDegree_add_C` `reflect_add` `reflect_C`
`reverse_eq_zero` 📖	mathematical	—	`reverse` `Polynomial` `instZero`	—	—
`reverse_leadingCoeff` 📖	mathematical	—	`leadingCoeff` `reverse` `trailingCoeff`	—	`leadingCoeff.eq_1` `reverse_natDegree` `revAt_le` `natTrailingDegree_le_natDegree` `coeff_reverse` `revAt_invol` `trailingCoeff.eq_1`
`reverse_mul` 📖	mathematical	—	`reverse` `Polynomial` `instMul`	—	`natDegree_mul'` `reflect_mul` `Eq.le`
`reverse_mul_X` 📖	mathematical	—	`reverse` `Polynomial` `instMul` `X`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `reverse_mul_of_domain` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `Subsingleton.to_isCancelMulZero` `Unique.instSubsingleton` `eq_or_ne` `MulZeroClass.zero_mul` `natDegree_mul_X` `reflect_mul` `natDegree_X` `reflect_one_X` `mul_one`
`reverse_mul_X_pow` 📖	mathematical	—	`reverse` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`pow_zero` `mul_one` `pow_succ` `mul_assoc` `reverse_mul_X`
`reverse_mul_of_domain` 📖	mathematical	—	`reverse` `Polynomial` `instMul`	—	`MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `reverse_zero` `reverse_mul`
`reverse_natDegree` 📖	mathematical	—	`natDegree` `reverse` `natTrailingDegree`	—	`natDegree_eq_reverse_natDegree_add_natTrailingDegree` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`reverse_natDegree_le` 📖	mathematical	—	`natDegree` `reverse`	—	`natDegree_le_iff_degree_le` `degree_le_iff_coeff_zero` `coeff_reverse` `revAt.eq_1` `not_le_of_gt` `Nat.cast_lt` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `coeff_eq_zero_of_natDegree_lt`
`reverse_neg` 📖	mathematical	—	`reverse` `Ring.toSemiring` `Polynomial` `instNeg`	—	`reverse.eq_1` `reflect_neg` `natDegree_neg`
`reverse_trailingCoeff` 📖	mathematical	—	`trailingCoeff` `reverse` `leadingCoeff`	—	`trailingCoeff.eq_1` `natTrailingDegree_reverse` `coeff_zero_reverse`
`reverse_zero` 📖	mathematical	—	`reverse` `Polynomial` `instZero`	—	—
`trailingCoeff_mul` 📖	mathematical	—	`trailingCoeff` `Polynomial` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`reverse_leadingCoeff` `reverse_mul_of_domain` `leadingCoeff_mul`

---

← Back to Index