toPrincipalIdeal_eq_iff — Mathlib

English

An element I of units in fractional ideals lies in the range of toPrincipalIdeal if and only if there exists x with spanSingleton(x) = I.

Русский

Элемент I в единицах фракционных идеалов принадлежит образу toPrincipalIdeal тогда и только тогда, когда существует x такой, что spanSingleton(x) = I.

LaTeX

$$I ∈ (toPrincipalIdeal R K).range \iff ∃ x : K, spanSingleton R⁰ x = I$$

Lean4

@[simp]
theorem toPrincipalIdeal_eq_iff {I : (FractionalIdeal R⁰ K)ˣ} {x : Kˣ} :
    toPrincipalIdeal R K x = I ↔ spanSingleton R⁰ (x : K) = I := by simp only [toPrincipalIdeal]; exact Units.ext_iff

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