le_colon

Mathlib.RingTheory.Ideal.Colon

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

← MathLib Explorer

English

For any two-sided ideal I, I ≤ I.colon J for all J.

Русский

Для любого двустороннего идеала I выполняется I ≤ I.colon J для любого J.

LaTeX

$$I ≤ I.colon J$$

Lean4

theorem _root_.Ideal.le_colon {I J : Ideal R} [I.IsTwoSided] : I ≤ I.colon J := by
  calc
    I = I.colon ⊤ := colon_top.symm
    _ ≤ I.colon J := colon_mono (le_refl I) le_top

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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