asIdeal_toTwoSided

Mathlib.RingTheory.TwoSidedIdeal.Operations

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

English

The composite of asIdeal followed by toTwoSided recovers the original two-sided ideal.

Русский

Составление asIdeal затем toTwoSided восстанавливает исходный двусторонний идеал.

LaTeX

$$$I.asIdeal.toTwoSided = I$$$

Lean4

@[simp]
theorem asIdeal_toTwoSided (I : Ideal R) [I.IsTwoSided] : I.toTwoSided.asIdeal = I :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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