isAlgebraic

Mathlib.RingTheory.Algebraic.Integral

URI: https://scilib.ai/kg/mathlib#Algebra.IsPushout.isAlgebraic

English

If [IsPushout R S R' S'], then Algebra.IsAlgebraic R' S' holds; i.e., algebraicity is inherited through pushouts.

Русский

Если выполняется IsPushout( R,S,R',S' ), то S' алгебраично над R'.

LaTeX

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

Lean4

theorem isAlgebraic [h : IsPushout R S R' S'] : Algebra.IsAlgebraic R' S' :=
  have := h.symm;
  (equiv R R' S S').isAlgebraic

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

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

Разделы

Аффилиация

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