baseChange_ring

Mathlib.RingTheory.Extension.Presentation.Submersive

URI: https://scilib.ai/kg/mathlib#Algebra.PreSubmersivePresentation.baseChange_ring

English

The underlying ring of the base-changed presentation is unchanged by base-change: Ring(baseChange(P)) = Ring(P).

Русский

Основание кольца базового изменения презентации сохраняется: Ring(baseChange(P)) = Ring(P).

LaTeX

$$$\\mathrm{Ring}(\\mathrm{baseChange}(P)) = \\mathrm{Ring}(P).$$$

Lean4

theorem baseChange_ring : (P.baseChange R).Ring = P.Ring :=
  rfl

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

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

Разделы

Аффилиация

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