fractionalIdeal_rank — Mathlib

English

Let K be a number field with ring of integers 𝓞K. For any fractional ideal I of 𝓞K (i.e., an invertible fractional ideal of 𝓞K), the underlying ℤ-module I has the same finite rank as 𝓞K itself. Equivalently, as a ℤ-module, the fractional ideal I has rank equal to the rank of 𝓞K.

Русский

Пусть K — число поля, кольцо целых чисел 𝓞K. Для любого дробного идеала I над 𝓞K (двоичный дробный идеал) как ℤ-модуль выполняется равенство рангов: он равен рангу самого 𝓞K.

LaTeX

$$$\\operatorname{finrank}_{\\mathbb{Z}}(I) \;=\; \\operatorname{finrank}_{\\mathbb{Z}}(\\mathcal{O}_K).$$$

Lean4

theorem fractionalIdeal_rank (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) : finrank ℤ I = finrank ℤ (𝓞 K) := by
  rw [finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, finrank_eq_card_basis (basisOfFractionalIdeal K I)]

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