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.