under_under

Mathlib.RingTheory.Ideal.Over

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

English

Contraction is associative: (P under B) under A = P under A.

Русский

Сжатия ассоциативны: (P.under B).under A = P.under A.

LaTeX

$$$ (\\mathfrak{P}.under B).under A = \\mathfrak{P}.under A. $$$

Lean4

@[simp]
theorem under_under : (𝔓.under B).under A = 𝔓.under A := by simp_rw [comap_comap, ← IsScalarTower.algebraMap_eq]

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

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

Разделы

Аффилиация

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