algebra_finiteType_of_liesOver — Mathlib

English

If B is a finitely generated A-algebra, then B/P is finitely generated over A/p when P lies over p.

Русский

Если B — конечная A-алгебра, то B/P — конечная над A/p, если P LiesOver p.

LaTeX

$$$\\text{Algebra.FiniteType } A B \\Rightarrow \\text{Algebra.FiniteType } (A/p) (B/P)$$$

Lean4

/-- `B ⧸ P` is a finitely generated `A ⧸ p`-algebra if `B` is a finitely generated `A`-algebra. -/
instance algebra_finiteType_of_liesOver [Algebra.FiniteType A B] : Algebra.FiniteType (A ⧸ p) (B ⧸ P) :=
  Algebra.FiniteType.of_restrictScalars_finiteType A (A ⧸ p) (B ⧸ P)

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