fractionalIdealBasis — Mathlib

English

There is a canonical ℤ-basis for a fractional ideal, obtained via an equivalence with a localized module and its basis.

Русский

Существует каноническая база дробного идеала над ℤ, получаемая через эквиваленцию с локализованным модулем и базисом.

LaTeX

$$$\\text{basisOfFractionalIdeal}$$$

Lean4

/-- A `ℤ`-basis of a fractional ideal. -/
noncomputable def fractionalIdealBasis (I : FractionalIdeal (𝓞 K)⁰ K) : Basis (Free.ChooseBasisIndex ℤ I) ℤ I :=
  Free.chooseBasis ℤ I

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