basisOfFractionalIdeal — Mathlib

English

There is a ℚ-basis for the fractional ideal I, compatible with a ℤ-basis via localization restricting scalars.

Русский

Существует ℚ-база дробного идеала I, совместимая с ℤ-базой через локализацию и ограничение скаляра.

LaTeX

$$$\\text{basisOfFractionalIdeal}(I) \\text{ is a } \\mathbb{Q}\\text{-basis compatible with } \\mathbb{Z}\\text{-basis}$$$

Lean4

/-- A `ℚ`-basis of `K` that spans `I` over `ℤ`, see `mem_span_basisOfFractionalIdeal` below. -/
noncomputable def basisOfFractionalIdeal (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) : Basis (Free.ChooseBasisIndex ℤ I) ℚ K :=
  (fractionalIdealBasis K I.1).ofIsLocalizedModule ℚ ℤ⁰ ((Submodule.subtype (I : Submodule (𝓞 K) K)).restrictScalars ℤ)

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