liesOver

Mathlib.RingTheory.Ideal.Over

URI: https://scilib.ai/kg/mathlib#Ideal.primesOver.liesOver

English

For any Q in primesOver p B, Q lies over p.

Русский

Для любого Q в primesOver p B, Q лежит над p.

LaTeX

$$forall Q ∈ p.primesOver B, Q.val.LiesOver(p)$$

Lean4

instance liesOver (Q : primesOver p B) : Q.1.LiesOver p :=
  Q.2.2

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

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

Разделы

Аффилиация

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