isPrime

Mathlib.RingTheory.Ideal.Over

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

English

If Q ∈ primesOver p B, then Q.1.LiesOver p.

Русский

Если Q ∈ primesOver p B, то Q.1 лежит над p.

LaTeX

$$$Q \in p.primesOver B \Rightarrow Q.1.LiesOver(p)$$$

Lean4

instance isPrime (Q : primesOver p B) : Q.1.IsPrime :=
  Q.2.1

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

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

Разделы

Аффилиация

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