instIsPushoutFractionRingMvPolynomial_1

English

There is an IsPushout instance for R, S with FractionRing(Polynomial R) and FractionRing(Polynomial S): pushout property holds after polynomial localization.

Русский

Существует инстанс IsPushout для R, S и FractionRing(Polynomial R), FractionRing(Polynomial S); свойство пушаута сохраняется после локализации полиномов.

LaTeX

$$$Algebra.IsPushout\;R\;S\;(FractionRing(Polynomial R))\;(FractionRing(Polynomial S))$$$

Lean4

instance {σ : Type*} : Algebra.IsPushout R S (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) :=
  .symm inferInstance

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