instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc

English

The ringOfIntegers Fq F is Noetherian as an algebra over F_q[X] under the separability hypothesis of RatFunc F_q over F.

Русский

Кольцо целых ringOfIntegers F_q F является Ноetherian как алгебра над F_q[X] при условии сепарируемости RatFunc F_q над F.

LaTeX

$$$\operatorname{IsNoetherian}_{F_q[X]}(\mathrm{ringOfIntegers}_{F_q}F).$$$

Lean4

instance [Algebra.IsSeparable (RatFunc Fq) F] : IsNoetherian Fq[X] (ringOfIntegers Fq F) :=
  IsIntegralClosure.isNoetherian _ (RatFunc Fq) F _

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