extendScalars_top — Mathlib

English

For any intermediate field F of L over K, extending scalars along the top relation yields the top intermediate field; i.e., extendScalars(le_top) = top.

Русский

Для любого промежуточного поля F между K и L, расширение скаляров по отношению к верхнему элементу даёт верхнее промежуточное поле; то есть extendScalars(le_top) = ⊤.

LaTeX

$$$\operatorname{extendScalars}(\le_{F}^{\top}) = \top$$$

Lean4

@[simp]
theorem extendScalars_top : extendScalars (le_top : F ≤ ⊤) = ⊤ :=
  restrictScalars_injective K (by simp)

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