instIsPushout_1

Mathlib.RingTheory.IsTensorProduct

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

English

The pushout construction is compatible with algebra isomorphisms, giving a functorial pushout.

Русский

Пушаут-конструкция совместима с алгебраическими изоморфизмами, образуя функторный пушаут.

LaTeX

$$Algebra.IsPushout.of_equiv$$

Lean4

instance : Algebra.IsPushout R S R S :=
  .symm inferInstance

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

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

Разделы

Аффилиация

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