count_maximal — Mathlib

English

For any w, count(K, v, w.asIdeal) equals 1 if w = v and 0 otherwise.

Русский

Для любого w: count(K, v, w.asIdeal) равно 1 если w = v, иначе 0.

LaTeX

$$$$ \\operatorname{count}(K,v, w.asIdeal) = \\begin{cases} 1, & w = v, \\\\ 0, & w \\neq v. \\end{cases} $$$$

Lean4

theorem count_maximal (w : HeightOneSpectrum R) [Decidable (w = v)] :
    count K v (w.asIdeal : FractionalIdeal R⁰ K) = if w = v then 1 else 0 :=
  by
  split_ifs with h
  · rw [h, count_self]
  · exact count_maximal_coprime K v h

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