instIsPushout_1

Mathlib.RingTheory.TensorProduct.MvPolynomial

URI: https://scilib.ai/kg/mathlib#MvPolynomial.instIsPushout_1

English

There is an instance declaring IsPushout for MvPolynomial with the appropriate algebra structure.

Русский

Для MvPolynomial существует экземпляр IsPushout с корректной алгебраической структурой.

LaTeX

$$Algebra.IsPushout R (MvPolynomial σ R) S (MvPolynomial σ S)$$

Lean4

instance : Algebra.IsPushout R (MvPolynomial σ R) S (MvPolynomial σ S) :=
  .symm inferInstance

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

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

Разделы

Аффилиация

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