lift_adjoin — Mathlib

English

For a field F and E with an F-algebra structure and S ⊆ E, lift of the adjoin equals adjoin of the set of target-values from S: lift (adjoin F S) = adjoin F ((Subtype.val) '' S).

Русский

Для поля F и расширения E с структурой F-алгебры и S ⊆ E, подъём адъюнта равен адъюнту образа S под отображение: lift (adjoin F S) = adjoin F ((Subtype.val) '' S).

LaTeX

$$$\\\\operatorname{lift} (\\\\operatorname{adjoin}_F S) = \\\\operatorname{adjoin}_F (\\\\operatorname{Subtype.val} '' S).$$$

Lean4

@[simp]
theorem lift_adjoin (K : IntermediateField F E) (S : Set K) : lift (adjoin F S) = adjoin F (Subtype.val '' S) :=
  adjoin_map _ _ _

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