finite_setOf_absNorm_le — Mathlib

English

For a fixed n, the set { I ∈ Ideal(S) | absNorm(I) = n } is finite.

Русский

Для фиксированного n множество { I ∈ Ideal(S) | absNorm(I) = n } конечно.

LaTeX

$$$$\{ I\in \mathrm{Ideal}(S) \mid \operatorname{absNorm}(I)=n\} \text{finite}.$$$$

Lean4

theorem finite_setOf_absNorm_le [CharZero S] (n : ℕ) : {I : Ideal S | Ideal.absNorm I ≤ n}.Finite :=
  by
  rw [show {I : Ideal S | Ideal.absNorm I ≤ n} = (⋃ i ∈ Set.Icc 0 n, {I : Ideal S | Ideal.absNorm I = i}) by ext; simp]
  refine Set.Finite.biUnion (Set.finite_Icc 0 n) (fun i _ => Ideal.finite_setOf_absNorm_eq i)

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