# 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

- MvPolynomial.invertibleC σ r = Invertible.map MvPolynomial.C r

noncomputable instance
MvPolynomial.invertibleCoeNat
(σ : Type u_1)
(R : Type u_2)
(p : ℕ)
[CommSemiring R]
[Invertible ↑p]
:

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.