restrictScalars_sup — Mathlib

English

Restriction distributes over the supremum: restricting scalars commutes with taking the supremum.

Русский

Ограничение скаляров распределяется по верхней границе: ограничение скаляров и взятие верхней границы совместимы.

LaTeX

$$$ L.restrictScalars K \\; \\sqcup \\; L'.restrictScalars K = (L \\sqcup L').restrictScalars K $$$

Lean4

theorem restrictScalars_sup : L.restrictScalars K ⊔ L'.restrictScalars K = (L ⊔ L').restrictScalars K :=
  toSubfield_injective (by simp)

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