under_liesOver_of_liesOver

Mathlib.RingTheory.Ideal.Over

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

English

If 𝔓 lies over 𝔓, then the under of 𝔓 lies over the same base ideal.

Русский

Если 𝔓 лежит над 𝔓, то under_B(𝔓) лежит над тем же основанием.

LaTeX

$$$ (\\mathfrak{P}.under B).LiesOver p. $$$

Lean4

instance under_liesOver_of_liesOver [𝔓.LiesOver p] : (𝔓.under B).LiesOver p :=
  LiesOver.tower_bot 𝔓 (𝔓.under B) p

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

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

Разделы

Аффилиация

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