Invertible polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file is a stub containing some basic facts about invertible elements in the ring of polynomials.
@[protected, instance]
noncomputable
def
mv_polynomial.invertible_C
(σ : Type u_1)
{R : Type u_2}
[comm_semiring R]
(r : R)
[invertible r] :
Equations
@[protected, instance]
noncomputable
def
mv_polynomial.invertible_coe_nat
(σ : Type u_1)
(R : Type u_2)
(p : ℕ)
[comm_semiring 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.