primesOver_finite — Mathlib

English

There is a finite type structure on p.primesOver B, i.e., the set of primes over p is finite and can be treated as a finite type.

Русский

Существуют структура конечного типа на множества primesOver p в B.

LaTeX

$$Fintype (p.primesOver B).Elem$$

Lean4

theorem primesOver_finite : (primesOver p B).Finite :=
  by
  by_cases hpb : p = ⊥
  · rw [hpb] at hpm ⊢
    haveI : IsDomain A := IsDomain.of_bot_isPrime A
    rw [primesOver_bot A B]
    exact Set.finite_singleton ⊥
  · rw [← coe_primesOverFinset hpb B]
    exact (primesOverFinset p B).finite_toSet

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