instIsPushoutPolynomial_1

Mathlib.RingTheory.PolynomialAlgebra

URI: https://scilib.ai/kg/mathlib#instIsPushoutPolynomial_1

English

The analogous pushout property holds when swapping the roles of R and R[X] with S and S[X], i.e., Algebra.IsPushout R R[X] S S[X].

Русский

Аналогичное свойство пуш-аута сохраняется при замене ролей R и R[X] на S и S[X], то есть Algebra.IsPushout R R[X] S S[X].

LaTeX

$$$\text{Algebra.IsPushout } R \ R[X] \ S \ S[X].$$$

Lean4

instance : Algebra.IsPushout R R[X] S S[X] :=
  .symm inferInstance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru