instIsPushoutFractionRingPolynomial

English

For any σ, the square R ⟶ FractionRing(MvPolynomial σ R) and S ⟶ FractionRing(MvPolynomial σ S) forms a pushout; i.e., the pushout property carries through to MV-polynomials after localization.

Русский

Для любого σ квадрат R → FractionRing(MvPolynomial σ R) и S → FractionRing(MvPolynomial σ S) образуют пушаут; то есть свойство пушаута сохраняется после локализации MV-полиномов.

LaTeX

$$$Algebra.IsPushout\;R\;S\;(FractionRing(\,MvPolynomial\;σ\;R))\;(FractionRing(\,MvPolynomial\;σ\;S))$$$

Lean4

instance : Algebra.IsPushout R (FractionRing R[X]) S (FractionRing S[X]) :=
  (Algebra.IsPushout.comp_iff _ R[X] _ S[X]).mpr inferInstance

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