card_infinitePlace_eq_card_infinitePlace

English

The rank of Units in the CM-field K over K⁺ equals the rank of Units in K; i.e., Units.rank(K⁺) = Units.rank(K).

Русский

Ранг группы единиц CM‑поля K над K⁺ равен рангу самих единиц: Units.rank(K⁺) = Units.rank(K).

LaTeX

$$$\\operatorname{Units.rank}(K^+) = \\operatorname{Units.rank}(K).$$$

Lean4

theorem card_infinitePlace_eq_card_infinitePlace : Fintype.card (InfinitePlace K⁺) = Fintype.card (InfinitePlace K) :=
  by
  rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add, add_zero, ←
    IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two, ← IsTotallyComplex.finrank, ←
    Module.finrank_mul_finrank ℚ K⁺ K, mul_comm, IsQuadraticExtension.finrank_eq_two _ K]

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