ne_bot_of_liesOver_of_ne_bot

Mathlib.RingTheory.Ideal.Over

URI: https://scilib.ai/kg/mathlib#Ideal.ne_bot_of_liesOver_of_ne_bot

English

If p ≠ ⊥ and P lies over p, then P ≠ ⊥.

Русский

Если p ≠ ⊥ и P лежит над p, то P ≠ ⊥.

LaTeX

$$$ p \\neq \\bot \\Rightarrow P \\neq \\bot. $$$

Lean4

theorem ne_bot_of_liesOver_of_ne_bot (hp : p ≠ ⊥) (P : Ideal B) [P.LiesOver p] : P ≠ ⊥ :=
  by
  contrapose! hp
  rw [over_def P p, hp, under_bot]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru