integralBasis — Mathlib

English

There exists a basis of K over ℚ which is also a basis of 𝓞K over ℤ; i.e., a single basis serves both as a ℚ-basis of K and a ℤ-basis of the ring of integers 𝓞K.

Русский

Существует базис K над ℚ, который одновременно является базисом 𝓞K над ℤ; один и тот же базис служит как для обоих структур.

LaTeX

$$$\\text{There exists a Basis } B \\text{ of } K \\text{ over } \\mathbb{Q} \\text{ that is also a } \\mathbb{Z}\\text{-basis of } \\mathcal{O}_K.$$$

Lean4

/-- A basis of `K` over `ℚ` that is also a basis of `𝓞 K` over `ℤ`. -/
noncomputable def integralBasis : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K :=
  Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) K (RingOfIntegers.basis K)

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