mathlib documentation


Invertible polynomials #

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

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.