lift_adjoin_simple — Mathlib

English

If α ∈ E and α ∈ K under some intermediate field K, then lift of adjoin F {α} equals adjoin F {α} (as α ∈ E).

Русский

Пусть α ∈ E и α принадлежит K; тогда lift(adjoin F {α}) = adjoin F {α}.

LaTeX

$$$\\\\operatorname{lift} (\\\\operatorname{adjoin}_F {\\\\alpha}) = \\\\operatorname{adjoin}_F {\\\\alpha.1}.$$$

Lean4

theorem lift_adjoin_simple (K : IntermediateField F E) (α : K) : lift (adjoin F { α }) = adjoin F { α.1 } := by
  simp only [lift_adjoin, Set.image_singleton]

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