extendScalars_restrictScalars

Mathlib.FieldTheory.IntermediateField.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.extendScalars_restrictScalars

English

Restrict back to K recovers the original E: (extendScalars(h)).restrictScalars K = E.

Русский

Обратное ограничения к K восстанавливает исходное E: (extendScalars(h)).restrictScalars K = E.

LaTeX

$$$(extendScalars(h)).restrictScalars K = E$$$

Lean4

@[simp]
theorem extendScalars_restrictScalars : (extendScalars h).restrictScalars K = E :=
  rfl

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

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

Разделы

Аффилиация

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