instIsPushout_1

Mathlib.RingTheory.Algebraic.Integral

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

English

If R ⟶ S is algebraic and the pushout square with R′, S′ exists, then the extension R′ ⟶ S′ is algebraic.

Русский

Если R ⟶ S алгебраическое и существует пушаутовый квадрат с R′, S′, то расширение R′ ⟶ S′ алгебраическое.

LaTeX

$$$IsPushout(R,S,R',S') \Rightarrow Algebra.IsAlgebraic(R',S')$$$

Lean4

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

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

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

Разделы

Аффилиация

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