toTwoSided_asIdeal

Mathlib.RingTheory.TwoSidedIdeal.Operations

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

English

The carrier of the two-sided version of an ideal equals the carrier of the original ideal.

Русский

Множество элементов двухстороннего варианта идеала совпадает с множеством исходного идеала.

LaTeX

$$$(I.toTwoSided : Set R) = Submodule.setLike.coe I$$$

Lean4

@[simp]
theorem toTwoSided_asIdeal (I : TwoSidedIdeal R) : I.asIdeal.toTwoSided = I := by ext; simp

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

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

Разделы

Аффилиация

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