trans — Mathlib

English

If S is a finite type over R and A is a finite type over S, then A is finite type over R.

Русский

Если S - конечная по типу над R, а A - конечная по типу над S, то A конечна по типу над R.

LaTeX

$$$\\text{FiniteType } R S \\land \\text{FiniteType } S A \\Rightarrow \\text{FiniteType } R A$$$

Lean4

theorem trans [Algebra S A] [IsScalarTower R S A] (hRS : FiniteType R S) (hSA : FiniteType S A) : FiniteType R A :=
  ⟨fg_trans' hRS.1 hSA.1⟩

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