Theorems · Definition · field theory

LaurentPolynomial.T

{R : Type u_1} → [inst : Semiring R] → ℤ → LaurentPolynomial R

The function n ↦ T ^ n, implemented as a sequence ℤ → R[T;T⁻¹]. Using directly T ^ n does not work, since we want the exponents to be of Type ℤ and there is no ℤ-power defined on R[T;T⁻¹]. Using that T is a unit introduces extra coercions. For these reasons, the definition of T is as a sequence.

Defined in

Mathlib.Algebra.Polynomial.Laurent

Cited by

55 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring