Roots of Laurent polynomials #
Let S be an R-algebra such that IsDomain S and FaithfulSMul R S. Then a Laurent polynomial
over R is determined by its evaluations (via LaurentPolynomial.smeval) at the units of S, as
soon as there are infinitely many of them: this is the analogue for R[T;T⁻¹] of
Polynomial.eq_zero_of_infinite_isRoot.
Main results #
LaurentPolynomial.eq_zero_of_infinite_smeval_eq_zero: a Laurent polynomial vanishing at infinitely many units is zero.LaurentPolynomial.eq_of_infinite_smeval_eq: two Laurent polynomials agreeing at infinitely many units are equal.
theorem LaurentPolynomial.eq_zero_of_infinite_smeval_eq_zero {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommRing S] [IsDomain S] [Algebra R S] [FaithfulSMul R S] (p : LaurentPolynomial R) (h : {x : Sˣ | p.smeval x = 0}.Infinite) :
A Laurent polynomial vanishing at infinitely many units is zero.
theorem LaurentPolynomial.eq_of_infinite_smeval_eq {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommRing S] [IsDomain S] [Algebra R S] [FaithfulSMul R S] {p q : LaurentPolynomial R} (h : {x : Sˣ | p.smeval x = q.smeval x}.Infinite) :
Two Laurent polynomials agreeing at infinitely many units are equal.