restrictScalars_adjoin_eq_sup — Mathlib

English

Restricting scalars of adjoin K S equals the supremum of K and adjoin F S: restrictScalars F (adjoin K S) = K ⊔ adjoin F S.

Русский

Ограничение скаляров от adjoin K S даёт верхнюю грань K и adjoin F S: restrictScalars F (adjoin K S) = K ⊔ adjoin F S.

LaTeX

$$$\\\\operatorname{restrictScalars} F (\\\\operatorname{adjoin} K S) = K \\\\sqcup \\\\operatorname{adjoin} F S.$$$

Lean4

theorem restrictScalars_adjoin_eq_sup (K : IntermediateField F E) (S : Set E) :
    restrictScalars F (adjoin K S) = K ⊔ adjoin F S := by rw [restrictScalars_adjoin, adjoin_union, adjoin_self]

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