instIsPushout — Mathlib

English

There is a pushout structure for MvPolynomial that identifies the left tensor with the right polynomial algebra via a canonical equivalence.

Русский

Существует структура pushout для MvPolynomial, которая идентифицирует левое тензорное произведение с правой полиномной алгеброй через каноническое эквивалентное отображение.

LaTeX

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

Lean4

instance : Algebra.IsPushout R S (MvPolynomial σ R) (MvPolynomial σ S) where
  out := .of_equiv (algebraTensorAlgEquiv R S).toLinearEquiv fun _ ↦ by simp

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