map_id'

Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

URI: https://scilib.ai/kg/mathlib#PrimeSpectrum.BasicConstructibleSetData.map_id'

English

Map with id equals identity for basic constructible set data.

Русский

Отображение с id для базовых данных конструктивного множества совпадает с тождественным отображением.

LaTeX

$$map (.id R) = id$$

Lean4

@[simp]
theorem map_id' : map (.id R) = id := by ext : 1; simp

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

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

Разделы

Аффилиация

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