invertibleCoeNat — Mathlib

English

A natural number p invertible in R is invertible when coerced into the polynomial ring MvPolynomial σ R.

Русский

Натуральное число p, обратимо в R, обратимо и после представления его как элемент MvPolynomial σ R.

LaTeX

$$$\text{Invertible}(p : \operatorname{MvPolynomial}(\sigma,R))$$$

Lean4

/-- 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. -/
noncomputable instance invertibleCoeNat (σ R : Type*) (p : ℕ) [CommSemiring R] [Invertible (p : R)] :
    Invertible (p : MvPolynomial σ R) :=
  IsScalarTower.invertibleAlgebraCoeNat R _ _

Похожие утверждения