fg_of_noetherian — Mathlib

English

The image of liftAlgHom is the intermediate field generated by the image of the base algebra hom g.

Русский

Образ liftAlgHom есть промежуточное поле, порождённое образом алгебраической леммы g.

LaTeX

$$(liftAlgHom hg).fieldRange = \operatorname{IntermediateField.adjoin}_F (g.range)$$

Lean4

theorem fg_of_noetherian (S : IntermediateField F E) [IsNoetherian F E] : S.FG :=
  S.fg_of_fg_toSubalgebra S.toSubalgebra.fg_of_noetherian

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