nrRealPlaces_pos_of_odd_finrank — Mathlib

English

If finrank_Q K is odd, then there exists at least one real place of K, i.e., nrRealPlaces(K) > 0.

Русский

Если finrank_Q K нечетно, тогда у K есть хотя бы одно действительное место, т.е. nrRealPlaces(K) > 0.

LaTeX

$$$\operatorname{finrank}_{\mathbb{Q}} K \equiv 1 \pmod{2} \Rightarrow 0 < \operatorname{nrRealPlaces}(K)$$$

Lean4

theorem nrRealPlaces_pos_of_odd_finrank (h : Odd (finrank ℚ K)) : 0 < nrRealPlaces K :=
  by
  refine Nat.pos_of_ne_zero ?_
  by_contra hc
  refine (Nat.not_odd_iff_even.mpr ?_) h
  rw [← card_add_two_mul_card_eq_rank, hc, zero_add]
  exact even_two_mul (nrComplexPlaces K)

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