Documentation

Mathlib.Data.MvPolynomial.Invertible

Invertible polynomials #

This file is a stub containing some basic facts about invertible elements in the ring of polynomials.

noncomputable instance MvPolynomial.invertibleC (σ : Type u_1) {R : Type u_2} [CommSemiring R] (r : R) [Invertible r] :
Invertible (MvPolynomial.C r)
Equations
noncomputable instance MvPolynomial.invertibleCoeNat (σ : Type u_1) (R : Type u_2) (p : ) [CommSemiring R] [Invertible p] :

A natural number that is invertible when coerced to a commutative semiring R is also invertible when coerced to any polynomial ring with rational coefficients.

Short-cut for typeclass resolution.

Equations