restrictScalars_adjoin — Mathlib

English

Restricting scalars to F of the adjoin of K with S equals adjoining K ∪ S over F: restrictScalars F (adjoin K S) = adjoin F (K ∪ S).

Русский

Ограничение скаляров до F от адъюнта K с S равняется адъюнту F от K ∪ S: restrictScalars F (adjoin K S) = adjoin F (K ∪ S).

LaTeX

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

Lean4

theorem restrictScalars_adjoin (K : IntermediateField F E) (S : Set E) :
    restrictScalars F (adjoin K S) = adjoin F (K ∪ S) := by rw [← adjoin_self _ K, adjoin_adjoin_left, adjoin_self _ K]

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