Commit 2023-06-10 20:59 5a919533

View on Github →

feat: port Data.Polynomial.UnitTrinomial (#4948)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/UnitTrinomial.lean

added theorem Polynomial.IsUnitTrinomial.card_support_eq_three

added theorem Polynomial.IsUnitTrinomial.coeff_isUnit

added theorem Polynomial.IsUnitTrinomial.irreducible_aux1

added theorem Polynomial.IsUnitTrinomial.irreducible_aux2

added theorem Polynomial.IsUnitTrinomial.irreducible_aux3

added theorem Polynomial.IsUnitTrinomial.irreducible_of_coprime'

added theorem Polynomial.IsUnitTrinomial.irreducible_of_coprime

added theorem Polynomial.IsUnitTrinomial.irreducible_of_isCoprime

added theorem Polynomial.IsUnitTrinomial.leadingCoeff_isUnit

added theorem Polynomial.IsUnitTrinomial.ne_zero

added theorem Polynomial.IsUnitTrinomial.not_isUnit

added theorem Polynomial.IsUnitTrinomial.trailingCoeff_isUnit

added def Polynomial.IsUnitTrinomial

added theorem Polynomial.isUnitTrinomial_iff''

added theorem Polynomial.isUnitTrinomial_iff'

added theorem Polynomial.isUnitTrinomial_iff

added theorem Polynomial.trinomial_def

added theorem Polynomial.trinomial_leadingCoeff

added theorem Polynomial.trinomial_leading_coeff'

added theorem Polynomial.trinomial_middle_coeff

added theorem Polynomial.trinomial_mirror

added theorem Polynomial.trinomial_monic

added theorem Polynomial.trinomial_natDegree

added theorem Polynomial.trinomial_natTrailingDegree

added theorem Polynomial.trinomial_support

added theorem Polynomial.trinomial_trailingCoeff

added theorem Polynomial.trinomial_trailing_coeff'