adjoin_basis_eq_top — Mathlib

English

Let b be a basis of E over F indexed by ι. Then the intermediate field adjoined by the range of b equals the top field (i.e., E is generated by the basis elements).

Русский

Пусть b — база E/F индексированная по ι. Тогда подполе, порождаемое образами b, совпадает с верхним полем, то есть E порождается базисами.

LaTeX

$$$$\\operatorname{adjoin}_F(\\operatorname{range}(b)) = \\top$$$$

Lean4

theorem adjoin_basis_eq_top : adjoin F (range b) = ⊤ :=
  toSubalgebra_injective <|
    Subalgebra.toSubmodule_injective <|
      top_unique <| (Basis.span_eq b).ge.trans <| (Algebra.span_le_adjoin F _).trans <| algebra_adjoin_le_adjoin _ _

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