primesOver_ncard_ne_zero — Mathlib

English

A proof variant for finite index CRT using the finite set of prime factors.

Русский

Доказательство конечного CRT через конечный набор простых факторов.

LaTeX

$$proof of Finset CRT equivalence$$

Lean4

theorem primesOver_ncard_ne_zero : (primesOver p B).ncard ≠ 0 :=
  by
  rcases exists_ideal_liesOver_maximal_of_isIntegral p B with ⟨P, hPm, hp⟩
  exact Set.ncard_ne_zero_of_mem ⟨hPm.isPrime, hp⟩ (primesOver_finite p B)

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