algebra_isIntegral_of_liesOver — Mathlib

English

If p is maximal in A, there exists a maximal ideal P in B such that P lies over p.

Русский

Если p максимален в A, существует максимальный идеал P в B, лежащий над p.

LaTeX

$$$\exists P : \mathrm{Ideal}(B), \; \mathrm{IsMaximal}(P) \land P.\mathrm{LiesOver}(p)$$$

Lean4

/-- `B ⧸ P` is an integral `A ⧸ p`-algebra if `B` is a integral `A`-algebra. -/
instance algebra_isIntegral_of_liesOver : Algebra.IsIntegral (A ⧸ p) (B ⧸ P) :=
  Algebra.IsIntegral.tower_top A

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