count_one — Mathlib

English

The count of the unit ideal equals zero: count(K, v, 1) = 0.

Русский

Счёт единицы равен нулю: count(K, v, 1) = 0.

LaTeX

$$$$\\operatorname{count}(K,v,1)=0.$$$$

Lean4

/-- val_v(1) = 0. -/
theorem count_one : count K v (1 : FractionalIdeal R⁰ K) = 0 :=
  by
  have h1 : (1 : FractionalIdeal R⁰ K) = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑(1 : Ideal R) := by
    rw [(algebraMap R K).map_one, Ideal.one_eq_top, coeIdeal_top, mul_one, inv_one, spanSingleton_one]
  rw [count_well_defined K v one_ne_zero h1, Ideal.span_singleton_one, Ideal.one_eq_top, sub_self]

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