eq_bot_of_liesOver_bot — Mathlib

English

If B is integral over A and P lies over (⊥), then P equals (⊥) (under mild nontriviality hypotheses).

Русский

Пусть B интегрально над A и P лежит над ⊥. Тогда P = ⊥ при некоторых предположениях о ненулевости A и домене B.

LaTeX

$$$\mathrm{P.LiesOver}(\bot) \Rightarrow P = \bot$$$

Lean4

theorem eq_bot_of_liesOver_bot [Nontrivial A] [IsDomain B] [h : P.LiesOver (⊥ : Ideal A)] : P = ⊥ :=
  eq_bot_of_comap_eq_bot <| ((liesOver_iff _ _).mp h).symm

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