under_bot

Mathlib.RingTheory.Ideal.Over

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

English

The contraction of the bottom ideal is the bottom ideal: under_A(⊥_B) = ⊥_A.

Русский

Сжатие нижнего идеала равно нижнему идеалу: under_A(⊥_B) = ⊥_A.

LaTeX

$$$ under_A(\\bot_B) = \\bot_A. $$$

Lean4

@[simp]
theorem under_bot : under A (⊥ : Ideal B) = ⊥ :=
  comap_bot_of_injective (algebraMap A B) (FaithfulSMul.algebraMap_injective A B)

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

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

Разделы

Аффилиация

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