instFiniteDimensionalSubtypeMemSubfieldSubfield

English

The fixed-point subfield substructure FixedPoints.subfield G F is a finite-dimensional F-vector space, i.e., FiniteDimensional (FixedPoints.subfield G F) F.

Русский

Подполе фиксированных точек образует конечномерное пространство над F.

LaTeX

$$$\\text{FiniteDimensional}( \\operatorname{FixedPoints.subfield } G F, F)$$$

Lean4

instance : FiniteDimensional (subfield G F) F :=
  by
  cases nonempty_fintype G
  exact
    IsNoetherian.iff_fg.1 (IsNoetherian.iff_rank_lt_aleph0.2 <| (rank_le_card G F).trans_lt <| Cardinal.nat_lt_aleph0 _)

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