of_liesOver_isMaximal — Mathlib

English

If P is a maximal ideal in B, p in A with P lies over p, and p is maximal while P is prime, then P is maximal.

Русский

Пусть P — максимальный идеал B, p — идеал A, имеющийся над p, и p максимален, а P прост. Тогда P максимален.

LaTeX

$$$(P.LiesOver p) \land [p.IsMaximal] \land [P.IsPrime] \Rightarrow P.IsMaximal$$$

Lean4

theorem of_liesOver_isMaximal [hpm : p.IsMaximal] [P.IsPrime] : P.IsMaximal :=
  by
  rw [P.over_def p] at hpm
  exact isMaximal_of_isIntegral_of_isMaximal_comap P hpm

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