Theorems · Definition · field theory

LaurentPolynomial

(R : Type u_3) → [Semiring R] → Type (max u_3 0)

The semiring of Laurent polynomials with coefficients in the semiring R. We denote it by R[T;T⁻¹]. The ring homomorphism C : R →+* R[T;T⁻¹] includes R as the constant polynomials.

Defined in

Mathlib.Algebra.Polynomial.Laurent

Cited by

98 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

Semiring