finiteQuotientOfFreeOfNeBot — Mathlib

English

A nonzero ideal I in a free finite extension S of the integers yields a finite quotient S/I.

Русский

Неформально: не нулевая идеяI в свободном конечном расш. S над Z даёт конечный фактор-модуль S/I.

LaTeX

$$Finite (S/I)$$

Lean4

/-- A nonzero ideal over a free finite extension of `ℤ` has a finite quotient.
It can't be an instance because of the side condition `I ≠ ⊥`.
-/
theorem finiteQuotientOfFreeOfNeBot [Module.Free ℤ S] [Module.Finite ℤ S] (I : Ideal S) (hI : I ≠ ⊥) : Finite (S ⧸ I) :=
  let b := Module.Free.chooseBasis ℤ S
  Submodule.finiteQuotientOfFreeOfRankEq (I.restrictScalars ℤ) <| finrank_eq_finrank b I hI

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