eq_top_iff_of_liesOver

Mathlib.RingTheory.Ideal.Over

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

English

If P lies over p, then P is top if and only if p is top.

Русский

Если P лежит над p, то P равен верхнему тогда и только тогда, когда p равен верхнему.

LaTeX

$$$ P = \\top \\;\\iff\\; p = \\top \\quad (\\text{with } P.LiesOver p). $$$

Lean4

theorem eq_top_iff_of_liesOver [P.LiesOver p] : P = ⊤ ↔ p = ⊤ :=
  by
  rw [P.over_def p]
  exact comap_eq_top_iff.symm

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

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

Разделы

Аффилиация

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