trans

Mathlib.RingTheory.Ideal.Over

URI: https://scilib.ai/kg/mathlib#Ideal.LiesOver.trans

English

If 𝔓 lies over P and P lies over p, then 𝔓 lies over p.

Русский

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

LaTeX

$$$ (\\mathfrak{P} \\LiesOver P) \\land (P \\LiesOver p) \\Rightarrow \\mathfrak{P} \\LiesOver p. $$$

Lean4

theorem trans [𝔓.LiesOver P] [P.LiesOver p] : 𝔓.LiesOver p where over := by rw [P.over_def p, 𝔓.over_def P, under_under]

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

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

Разделы

Аффилиация

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