Documentation Verification Report

UnitTrinomial

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

Statistics

Metric	Count
Definitions `IsUnitTrinomial`, `trinomial`	2
Theorems `card_support_eq_three`, `coeff_isUnit`, `irreducible_aux1`, `irreducible_aux2`, `irreducible_aux3`, `irreducible_of_coprime`, `irreducible_of_isCoprime`, `leadingCoeff_isUnit`, `ne_zero`, `not_isUnit`, `trailingCoeff_isUnit`, `isUnitTrinomial_iff`, `isUnitTrinomial_iff'`, `isUnitTrinomial_iff''`, `trinomial_def`, `trinomial_leadingCoeff`, `trinomial_leading_coeff'`, `trinomial_middle_coeff`, `trinomial_mirror`, `trinomial_monic`, `trinomial_natDegree`, `trinomial_natTrailingDegree`, `trinomial_support`, `trinomial_trailingCoeff`, `trinomial_trailing_coeff'`	25
Total	27

Polynomial

Definitions

Name	Category	Theorems
`IsUnitTrinomial` 📖	MathDef	3 math math: `isUnitTrinomial_iff`, `isUnitTrinomial_iff''`, `isUnitTrinomial_iff'`
`trinomial` 📖	CompOp	11 math math: `trinomial_trailing_coeff'`, `trinomial_leading_coeff'`, `trinomial_natTrailingDegree`, `trinomial_natDegree`, `trinomial_trailingCoeff`, `trinomial_monic`, `trinomial_middle_coeff`, `trinomial_leadingCoeff`, `trinomial_def`, `trinomial_support`, `trinomial_mirror`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUnitTrinomial_iff` 📖	mathematical	—	`IsUnitTrinomial` `Finset.card` `support` `Int.instSemiring` `IsUnit` `Int.instMonoid` `coeff`	—	`IsUnitTrinomial.card_support_eq_three` `IsUnitTrinomial.coeff_isUnit` `card_support_eq_three` `support_trinomial` `Finset.mem_insert_self` `Finset.mem_insert_of_mem` `Finset.mem_singleton_self` `add_zero` `MulZeroClass.mul_zero` `LT.lt.ne` `LT.lt.trans` `coeff_X_pow` `mul_one` `coeff_X_pow_self` `coeff_C_mul` `coeff_add` `zero_add` `LT.lt.ne'`
`isUnitTrinomial_iff'` 📖	mathematical	—	`IsUnitTrinomial` `coeff` `Int.instSemiring` `Polynomial` `instMul` `mirror` `natDegree` `natTrailingDegree`	—	`natDegree_mul_mirror` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `natTrailingDegree_mul_mirror` `mul_add` `Distrib.leftDistribClass` `Nat.instAtLeastTwoHAddOfNat` `zero_lt_two` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `coeff_mul_mirror` `sum_def` `trinomial_support` `Units.ne_zero` `Int.instNontrivial` `Finset.sum_insert` `Finset.mem_insert` `LT.lt.ne` `Finset.mem_singleton` `LT.lt.trans` `Finset.sum_singleton` `trinomial_leading_coeff'` `trinomial_middle_coeff` `trinomial_trailing_coeff'` `Int.units_sq` `Int.sq_eq_one_of_sq_le_three` `LE.le.trans` `Finset.single_le_sum` `Int.instAddLeftMono` `sq_nonneg` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Eq.le` `mem_support_iff` `isUnitTrinomial_iff` `Nat.cast_injective` `Int.instCharZero` `Nat.smul_one_eq_cast` `Finset.sum_const` `Finset.sum_congr` `IsUnit.of_pow_eq_one` `two_ne_zero`
`isUnitTrinomial_iff''` 📖	mathematical	`Polynomial` `Int.instSemiring` `instMul` `mirror`	`IsUnitTrinomial`	—	`isUnitTrinomial_iff'`
`trinomial_def` 📖	mathematical	—	`trinomial` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	—
`trinomial_leadingCoeff` 📖	mathematical	—	`leadingCoeff` `trinomial`	—	`leadingCoeff.eq_1` `trinomial_natDegree` `trinomial_leading_coeff'`
`trinomial_leading_coeff'` 📖	mathematical	—	`coeff` `trinomial`	—	`trinomial_def` `coeff_add` `coeff_C_mul_X_pow` `LT.lt.ne'` `LT.lt.trans` `zero_add`
`trinomial_middle_coeff` 📖	mathematical	—	`coeff` `trinomial`	—	`trinomial_def` `coeff_add` `coeff_C_mul_X_pow` `LT.lt.ne'` `LT.lt.ne` `zero_add` `add_zero`
`trinomial_mirror` 📖	mathematical	—	`mirror` `trinomial`	—	`mirror.eq_1` `trinomial_natTrailingDegree` `reverse.eq_1` `trinomial_natDegree` `trinomial_def` `reflect_add` `reflect_C_mul_X_pow` `revAt_le` `LT.lt.le` `LT.lt.trans` `le_rfl` `add_mul` `Distrib.rightDistribClass` `mul_assoc` `pow_add` `zero_add` `add_comm` `add_assoc`
`trinomial_monic` 📖	mathematical	—	`Monic` `trinomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `trinomial_leadingCoeff` `one_ne_zero` `NeZero.one`
`trinomial_natDegree` 📖	mathematical	—	`natDegree` `trinomial`	—	`natDegree_eq_of_degree_eq_some` `LE.le.antisymm` `Finset.sup_le` `support_trinomial'` `Finset.mem_singleton` `Finset.mem_insert` `WithBot.coe_le_coe` `LT.lt.le` `LT.lt.trans` `le_rfl` `le_degree_of_ne_zero` `trinomial_leading_coeff'`
`trinomial_natTrailingDegree` 📖	mathematical	—	`natTrailingDegree` `trinomial`	—	`natTrailingDegree_eq_of_trailingDegree_eq_some` `LE.le.antisymm` `Finset.le_inf` `support_trinomial'` `Finset.mem_singleton` `Finset.mem_insert` `le_rfl` `WithTop.coe_le_coe` `LT.lt.le` `LT.lt.trans` `trailingDegree_le_of_ne_zero` `trinomial_trailing_coeff'`
`trinomial_support` 📖	mathematical	—	`support` `trinomial` `Finset` `Finset.instInsert` `Finset.instSingleton`	—	`support_trinomial`
`trinomial_trailingCoeff` 📖	mathematical	—	`trailingCoeff` `trinomial`	—	`trailingCoeff.eq_1` `trinomial_natTrailingDegree` `trinomial_trailing_coeff'`
`trinomial_trailing_coeff'` 📖	mathematical	—	`coeff` `trinomial`	—	`trinomial_def` `coeff_add` `coeff_C_mul_X_pow` `LT.lt.ne` `LT.lt.trans` `add_zero`

Polynomial.IsUnitTrinomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_support_eq_three` 📖	mathematical	`Polynomial.IsUnitTrinomial`	`Finset.card` `Polynomial.support` `Int.instSemiring`	—	`Polynomial.card_support_trinomial` `Units.ne_zero` `Int.instNontrivial`
`coeff_isUnit` 📖	mathematical	`Polynomial.IsUnitTrinomial` `Finset` `Finset.instMembership` `Polynomial.support` `Int.instSemiring`	`IsUnit` `Int.instMonoid` `Polynomial.coeff`	—	`Polynomial.support_trinomial'` `Finset.mem_singleton` `Finset.mem_insert` `Polynomial.trinomial_trailing_coeff'` `Polynomial.trinomial_middle_coeff` `Polynomial.trinomial_leading_coeff'`
`irreducible_aux1` 📖	mathematical	`Polynomial.trinomial` `Int.instSemiring` `Units.val` `Int.instMonoid`	`Polynomial` `Polynomial.instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.instAdd` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.X` `Polynomial.ofFinsupp` `Finsupp.filter` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Set` `Set.instMembership` `Set.Ioo` `Nat.instPreorder` `Set.decidableMemIoo` `Preorder.toLT` `Polynomial.toFinsupp` `Polynomial.mirror`	—	`lt_tsub_iff_right` `Nat.instOrderedSub` `tsub_lt_tsub_iff_left_of_le` `Nat.instCanonicallyOrderedAdd` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `LT.lt.le` `Polynomial.trinomial_mirror` `Units.ne_zero` `Int.instNontrivial` `Polynomial.C_mul_X_pow_eq_monomial` `Finsupp.filter.congr_simp` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `Polynomial.monomial_mul_monomial` `Polynomial.toFinsupp_add` `Polynomial.toFinsupp_monomial` `Finsupp.filter_add` `Finsupp.filter_single_of_neg` `asymm` `instAsymmLt` `add_lt_add_iff_left` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `LT.lt.trans` `LT.lt.ne` `add_assoc` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `add_comm` `Finsupp.filter_single_of_pos` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `lt_add_iff_pos_left` `contravariant_swap_add_of_contravariant_add` `tsub_pos_iff_lt` `add_lt_add_right` `add_zero` `zero_add` `Polynomial.ofFinsupp_add` `Polynomial.ofFinsupp_single` `Polynomial.C_mul_monomial` `mul_comm`
`irreducible_aux2` 📖	—	`Polynomial.trinomial` `Int.instSemiring` `Units.val` `Int.instMonoid` `Polynomial` `Polynomial.instMul` `Polynomial.mirror`	—	—	`irreducible_aux1` `AddRightCancelSemigroup.toIsRightCancelAdd` `Polynomial.binomial_eq_binomial` `Units.ne_zero` `Int.instNontrivial` `Polynomial.isUnit_C` `Units.isUnit` `Polynomial.mirror_eq_iff` `Polynomial.trinomial_mirror`
`irreducible_aux3` 📖	—	`Polynomial.trinomial` `Int.instSemiring` `Units.val` `Int.instMonoid` `Polynomial` `Polynomial.instMul` `Polynomial.mirror`	—	—	`Int.isUnit_add_isUnit_eq_isUnit_add_isUnit` `Units.isUnit` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `Int.instIsCancelMulZero` `mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `two_ne_zero` `Units.ne_zero` `Int.instNontrivial` `Nat.instAtLeastTwoHAddOfNat` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `mul_assoc` `Polynomial.trinomial_trailingCoeff` `Polynomial.trinomial_leadingCoeff` `Polynomial.mirror_leadingCoeff` `Polynomial.leadingCoeff_mul` `add_sq'` `Int.units_sq` `add_assoc` `add_comm` `Polynomial.eval_add` `Polynomial.eval_C_mul` `Polynomial.eval_X_pow` `one_pow` `mul_one` `sq` `Polynomial.mirror_eval_one` `Polynomial.eval_mul` `irreducible_aux2` `Polynomial.mirror_eq_iff` `lt_add_of_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `tsub_pos_of_lt` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `lt_tsub_iff_right` `tsub_lt_tsub_iff_left_of_le` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `LT.lt.le` `Polynomial.trinomial_mirror` `Polynomial.mirror_mirror` `mul_comm`
`irreducible_of_coprime` 📖	mathematical	`Polynomial.IsUnitTrinomial` `IsRelPrime` `Polynomial` `Int.instSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.mirror`	`Irreducible`	—	`Polynomial.irreducible_of_mirror` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `not_isUnit` `Polynomial.isUnitTrinomial_iff''` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `two_ne_zero` `Polynomial.trinomial_natTrailingDegree` `Units.ne_zero` `Int.instNontrivial` `Polynomial.natTrailingDegree_mul_mirror` `Polynomial.trinomial_natDegree` `Polynomial.natDegree_mul_mirror` `eq_or_eq_neg_of_sq_eq_sq` `Int.isUnit_sq` `Units.isUnit` `irreducible_aux3` `Polynomial.C_neg` `neg_mul` `neg_add` `Polynomial.trinomial_def` `Polynomial.mirror_neg` `neg_mul_neg`
`irreducible_of_isCoprime` 📖	mathematical	`Polynomial.IsUnitTrinomial` `IsCoprime` `Polynomial` `Int.instSemiring` `Polynomial.commSemiring` `Int.instCommSemiring` `Polynomial.mirror`	`Irreducible` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	—	`irreducible_of_coprime` `IsCoprime.isUnit_of_dvd'`
`leadingCoeff_isUnit` 📖	mathematical	`Polynomial.IsUnitTrinomial`	`IsUnit` `Int.instMonoid` `Polynomial.leadingCoeff` `Int.instSemiring`	—	`coeff_isUnit` `Polynomial.natDegree_mem_support_of_nonzero` `ne_zero`
`ne_zero` 📖	—	`Polynomial.IsUnitTrinomial`	—	—	`Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `card_support_eq_three`
`not_isUnit` 📖	mathematical	`Polynomial.IsUnitTrinomial`	`IsUnit` `Polynomial` `Int.instSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	—	`ne_zero_of_lt` `Polynomial.trinomial_natDegree` `Units.ne_zero` `Int.instNontrivial` `Polynomial.natDegree_eq_of_degree_eq_some` `Polynomial.degree_eq_zero_of_isUnit` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE`
`trailingCoeff_isUnit` 📖	mathematical	`Polynomial.IsUnitTrinomial`	`IsUnit` `Int.instMonoid` `Polynomial.trailingCoeff` `Int.instSemiring`	—	`coeff_isUnit` `Polynomial.natTrailingDegree_mem_support_of_nonzero` `ne_zero`

---

← Back to Index