extendScalars_top — Mathlib

English

The join of two scalar extensions equals the scalar extension of their join.

Русский

Объединение двух расширений скалярных равно расширению скалярных через их объединение.

LaTeX

$$$\operatorname{extendScalars} h \lor \operatorname{extendScalars} h' = \operatorname{extendScalars} (h \lor h')$$$

Lean4

@[simp]
theorem extendScalars_top : extendScalars (le_top : F ≤ ⊤) = ⊤ :=
  IntermediateField.toSubfield_injective (by simp)

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