mathlib3 documentation

data.mv_polynomial.invertible

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.

Equations