adjoin_simple_adjoin_simple — Mathlib

English

The fields generated by adjoining α and β over F commute up to restriction, i.e. F⟮α⟯⟮β⟯ ≃ F⟮β⟯⟮α⟯ after restricting scalars to F.

Русский

Поля, получаемые последовательной адъюнкцией α и β над F, коммутируют после редукции к F.

LaTeX

$$$F⟮α⟯⟮β⟯.restrictScalars F = F⟮β⟯⟮α⟯.restrictScalars F$$$

Lean4

theorem adjoin_simple_adjoin_simple (β : E) : F⟮α⟯⟮β⟯.restrictScalars F = F⟮α, β⟯ :=
  adjoin_adjoin_left _ _ _

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