finite_quotient_pow — Mathlib

English

Let s be a finite set of ring elements generating I (span s = I) and I ⟂ finite quotient. Then for every n, the index [I^n] is bounded by [I]^{∑_{i=0}^{n-1} |s|^i}.

Русский

Пусть s порождает I, и R/I конечно. Для каждого n выполнено: [I^n] ≤ [I]^{∑_{i=0}^{n-1} |s|^i}.

LaTeX

$$$$[R:I^n] \le [R:I]^{\sum_{i=0}^{n-1} |s|^i}.$$$$

Lean4

theorem finite_quotient_pow (hI : I.FG) [Finite (R ⧸ I)] (n) : Finite (R ⧸ I ^ n) := by
  induction n with
  | zero =>
    simp only [pow_zero, Ideal.one_eq_top]
    infer_instance
  | succ n _ => exact Submodule.finite_quotient_smul (I ^ n) hI

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