Mirror

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

Statistics

Metric	Count
Definitions `mirror`	1
Theorems `coeff_mirror`, `coeff_mul_mirror`, `irreducible_of_mirror`, `mirror_C`, `mirror_X`, `mirror_eq_iff`, `mirror_eq_zero`, `mirror_eval_one`, `mirror_inj`, `mirror_involutive`, `mirror_leadingCoeff`, `mirror_mirror`, `mirror_monomial`, `mirror_mul_of_domain`, `mirror_natDegree`, `mirror_natTrailingDegree`, `mirror_neg`, `mirror_smul`, `mirror_trailingCoeff`, `mirror_zero`, `natDegree_mul_mirror`, `natTrailingDegree_mul_mirror`	22
Total	23

Polynomial

Definitions

Name	Category	Theorems
`mirror` 📖	CompOp	24 math math: `mirror_X`, `mirror_trailingCoeff`, `mirror_neg`, `mirror_monomial`, `natDegree_mul_mirror`, `natTrailingDegree_mul_mirror`, `mirror_leadingCoeff`, `mirror_eq_iff`, `mirror_involutive`, `mirror_mul_of_domain`, `mirror_zero`, `mirror_natDegree`, `mirror_eval_one`, `mirror_eq_zero`, `coeff_mirror`, `mirror_natTrailingDegree`, `isUnitTrinomial_iff'`, `trinomial_mirror`, `mirror_smul`, `coeff_mul_mirror`, `IsUnitTrinomial.irreducible_aux1`, `mirror_C`, `mirror_inj`, `mirror_mirror`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_mirror` 📖	mathematical	—	`coeff` `mirror` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `revAt` `natDegree` `natTrailingDegree`	—	`coeff_eq_zero_of_natDegree_lt` `mirror_natDegree` `revAt_le` `coeff_eq_zero_of_lt_natTrailingDegree` `tsub_lt_iff_left` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `revAtFun_eq` `revAtFun.eq_1` `LE.le.trans` `not_lt` `tsub_add_eq_add_tsub` `tsub_tsub_assoc` `mirror.eq_1` `coeff_mul_X_pow'` `coeff_reverse` `tsub_le_self` `lt_tsub_iff_right` `not_le` `mirror_natTrailingDegree`
`coeff_mul_mirror` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `mirror` `natDegree` `natTrailingDegree` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`coeff_mul` `Finset.sum_congr` `coeff_mirror` `revAt_le` `Finset.mem_range_succ_iff` `revAt_invol` `sq` `sum_eq_of_subset` `zero_pow` `two_ne_zero` `LE.le.trans` `le_natDegree_of_mem_supp`
`irreducible_of_mirror` 📖	mathematical	`IsUnit` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instNeg` `CommRing.toRing` `mirror` `IsRelPrime`	`Irreducible`	—	`mirror_mul_of_domain` `mirror_mirror` `mul_assoc` `mul_comm` `dvd_mul_right` `dvd_mul_left` `neg_eq_iff_eq_neg` `mirror_neg` `dvd_neg`
`mirror_C` 📖	mathematical	—	`mirror` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`mirror_monomial`
`mirror_X` 📖	mathematical	—	`mirror` `X`	—	`mirror_monomial`
`mirror_eq_iff` 📖	mathematical	—	`mirror`	—	`Function.Involutive.eq_iff` `mirror_involutive`
`mirror_eq_zero` 📖	mathematical	—	`mirror` `Polynomial` `instZero`	—	`mirror_mirror` `mirror_zero`
`mirror_eval_one` 📖	mathematical	—	`eval` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `mirror`	—	`eval_eq_sum_range` `Finset.sum_congr` `one_pow` `mul_one` `mirror_natDegree` `Finset.sum_bij_ne_zero` `Finset.mem_range_succ_iff` `revAt_le` `LE.le.trans` `tsub_le_iff_tsub_le` `Nat.instOrderedSub` `add_comm` `add_tsub_cancel_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mirror_natTrailingDegree` `natTrailingDegree_le_of_ne_zero` `revAt_invol` `coeff_mirror`
`mirror_inj` 📖	mathematical	—	`mirror`	—	`Function.Involutive.injective` `mirror_involutive`
`mirror_involutive` 📖	mathematical	—	`Function.Involutive` `Polynomial` `mirror`	—	`mirror_mirror`
`mirror_leadingCoeff` 📖	mathematical	—	`leadingCoeff` `mirror` `trailingCoeff`	—	`mirror_mirror` `mirror_trailingCoeff`
`mirror_mirror` 📖	mathematical	—	`mirror`	—	`ext` `coeff_mirror` `mirror_natDegree` `mirror_natTrailingDegree` `revAt_invol`
`mirror_monomial` 📖	mathematical	—	`mirror` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	`monomial_zero_right` `mirror_zero` `mirror.eq_1` `reverse.eq_1` `natDegree_monomial` `natTrailingDegree_monomial` `C_mul_X_pow_eq_monomial` `reflect_C_mul_X_pow` `revAt_le` `le_refl` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `mul_one`
`mirror_mul_of_domain` 📖	mathematical	—	`mirror` `Ring.toSemiring` `Polynomial` `instMul`	—	`MulZeroClass.zero_mul` `mirror_zero` `MulZeroClass.mul_zero` `mirror.eq_1` `reverse_mul_of_domain` `natTrailingDegree_mul` `pow_add` `mul_assoc` `X_pow_mul`
`mirror_natDegree` 📖	mathematical	—	`natDegree` `mirror`	—	`mirror_zero` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `natDegree_of_subsingleton` `mirror.eq_1` `natDegree_mul'` `leadingCoeff_X_pow` `mul_one` `reverse_leadingCoeff` `trailingCoeff_eq_zero` `reverse_natDegree` `natDegree_X_pow` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `natTrailingDegree_le_natDegree`
`mirror_natTrailingDegree` 📖	mathematical	—	`natTrailingDegree` `mirror`	—	`mirror_zero` `mirror.eq_1` `natTrailingDegree_mul_X_pow` `reverse_eq_zero` `natTrailingDegree_reverse` `zero_add`
`mirror_neg` 📖	mathematical	—	`mirror` `Ring.toSemiring` `Polynomial` `instNeg`	—	`mirror.eq_1` `reverse_neg` `natTrailingDegree_neg` `neg_mul_eq_neg_mul`
`mirror_smul` 📖	mathematical	—	`mirror` `Ring.toSemiring` `Polynomial` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`C_mul'` `mirror_mul_of_domain` `mirror_C`
`mirror_trailingCoeff` 📖	mathematical	—	`trailingCoeff` `mirror` `leadingCoeff`	—	`leadingCoeff.eq_1` `trailingCoeff.eq_1` `mirror_natTrailingDegree` `coeff_mirror` `revAt_le` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`mirror_zero` 📖	mathematical	—	`mirror` `Polynomial` `instZero`	—	`pow_zero` `mul_one`
`natDegree_mul_mirror` 📖	mathematical	—	`natDegree` `Polynomial` `instMul` `mirror`	—	`MulZeroClass.zero_mul` `natDegree_zero` `MulZeroClass.mul_zero` `natDegree_mul` `mirror_eq_zero` `mirror_natDegree` `Nat.instAtLeastTwoHAddOfNat` `two_mul`
`natTrailingDegree_mul_mirror` 📖	mathematical	—	`natTrailingDegree` `Polynomial` `instMul` `mirror`	—	`MulZeroClass.zero_mul` `natTrailingDegree_zero` `MulZeroClass.mul_zero` `natTrailingDegree_mul` `mirror_eq_zero` `mirror_natTrailingDegree` `Nat.instAtLeastTwoHAddOfNat` `two_mul`

---

← Back to Index