Multivariate Laurent polynomials

This file defines Laurent polynomial rings over a base ring (or even semiring), with variables from a general type σ (which could be infinite).

@[reducible, inline]

abbrev MvLaurentPolynomial (σ : Type u_1) (R : Type u_2) [Semiring R] : Type (max u_2 u_1)

Equations

• MvLaurentPolynomial σ R = AddMonoidAlgebra R (FreeAbelianGroup σ)

noncomputable def MvLaurentPolynomial.liftEquiv (σ : Type u_1) (R : Type u_2) (S : Type u_3) [CommRing R] [CommRing S] [Algebra R S] : (σ → Sˣ) ≃* (MvLaurentPolynomial σ R →ₐ[R] S)

Equations

• One or more equations did not get rendered due to their size.