mem_span_basisOfFractionalIdeal — Mathlib

English

A precise equivalence between membership in a span of a basis and membership in the fractional ideal coerced to K.

Русский

Точная эквиваленция между принадлежностью элементa к линейной оболочке базы и принадлежностью элементa дробному идеалу внутри K.

LaTeX

$$x ∈ Submodule.span ℤ (Set.range (basisOfFractionalIdeal K I)) ↔ x ∈ (I : Set K)$$

Lean4

theorem mem_span_basisOfFractionalIdeal {I : (FractionalIdeal (𝓞 K)⁰ K)ˣ} {x : K} :
    x ∈ Submodule.span ℤ (Set.range (basisOfFractionalIdeal K I)) ↔ x ∈ (I : Set K) :=
  by
  rw [basisOfFractionalIdeal, (fractionalIdealBasis K I.1).ofIsLocalizedModule_span ℚ ℤ⁰ _]
  simp

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