basis — Mathlib

English

A ℤ-basis of 𝓞_K exists; equivalently, 𝓞_K has a free ℤ-basis.

Русский

Существует ℤ-базис 𝓞_K; то есть 𝓞_K свободно порождается над ℤ.

LaTeX

$$$\\text{basis} := \\mathrm{Basis}(\\mathrm{FreeChooseBasisIndex}(\\mathcal{O}_K), \\mathbb{Z}, \\mathcal{O}_K)$$$

Lean4

/-- A ℤ-basis of the ring of integers of `K`. -/
noncomputable def basis : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K) :=
  Free.chooseBasis ℤ (𝓞 K)

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