isAlgebraic' — Mathlib

English

If the square R ⟶ S and R′ ⟶ S′ forms a pushout, then S′ is algebraic over R′; this is captured by the equivalence with the algebraic property via the isomorphism of the pushout square.

Русский

Если квадрат R ⟶ S и R′ ⟶ S′ образуют пушаут, то S′ алгебраично над R′; это выражается через эквивалентность с алгебраичностью через изоморфизм пушаутного квадрата.

LaTeX

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

Lean4

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

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