colon_top

Mathlib.RingTheory.Ideal.Colon

URI: https://scilib.ai/kg/mathlib#Submodule.colon_top

← MathLib Explorer

English

I.colon ⊤ = I for any two-sided ideal I.

Русский

I.colon ⊤ = I для любого двустороннего идеала I.

LaTeX

$$I.colon ⊤ = I$$

Lean4

@[simp]
theorem colon_top {I : Ideal R} [I.IsTwoSided] : I.colon ⊤ = I :=
  by
  simp_rw [SetLike.ext_iff, mem_colon, smul_eq_mul]
  exact fun x ↦ ⟨fun h ↦ mul_one x ▸ h 1 trivial, fun h _ _ ↦ I.mul_mem_right _ h⟩

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

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

Разделы

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

Аффилиация

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