basisOfFractionalIdeal_apply — Mathlib

English

A lemma equates span relations of a basis of a fractional ideal with membership in the fractional ideal

Русский

Лемма приравнивает отношения порога порождения базы дробного идеала к принадлежности элементa дробному идеалу

LaTeX

$$$x \\in \\operatorname{span}_{\\mathbb{Z}}(\\{\\text{basisOfFractionalIdeal}\\}) \\iff x \\in I$$$

Lean4

theorem basisOfFractionalIdeal_apply (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) (i : Free.ChooseBasisIndex ℤ I) :
    basisOfFractionalIdeal K I i = fractionalIdealBasis K I.1 i :=
  (fractionalIdealBasis K I.1).ofIsLocalizedModule_apply ℚ ℤ⁰ _ i

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