trans — Mathlib

English

If A is integral over R and B is integral over A, then B is integral over R.

Русский

Если A интегрально над R, а B интегрально над A, то B интегрально над R.

LaTeX

$$$\text{Algebra.IsIntegral.R A} \land \text{Algebra.IsIntegral A B} \Rightarrow \text{Algebra.IsIntegral R B}$$$

Lean4

/-- If A is an R-algebra all of whose elements are integral over R,
and B is an A-algebra all of whose elements are integral over A,
then all elements of B are integral over R. -/
protected theorem trans [Algebra.IsIntegral R A] [Algebra.IsIntegral A B] : Algebra.IsIntegral R B :=
  ⟨fun x ↦ isIntegral_trans x (Algebra.IsIntegral.isIntegral (R := A) x)⟩

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