invertibleC — Mathlib

English

If a natural number r is invertible in a commutative semiring R, then its embedding as a constant polynomial Cr is invertible in the polynomial ring MvPolynomial σ R.

Русский

Если натуральное число r обратимо в коммутативном полускольном кольце R, то его константный полином Cr обратим в кольце MvPolynomial σ R.

LaTeX

$$$\text{invertible}(Cr)\text{ in } \operatorname{MvPolynomial}(\sigma,R)$$$

Lean4

noncomputable instance invertibleC (σ : Type*) {R : Type*} [CommSemiring R] (r : R) [Invertible r] :
    Invertible (C r : MvPolynomial σ R) :=
  Invertible.map (C : R →+* MvPolynomial σ R) _

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