mem_extended_iff

Mathlib.RingTheory.FractionalIdeal.Extended

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.mem_extended_iff

English

The extended fractional ideal equals the span of the image of I under the localization map.

Русский

Расширенный дробный идеал равен диапазону образа I под локализационной картой.

LaTeX

$$$I.extended L hf = \mathrm{span}_B (\mathrm{map}_f'' I)$$$

Lean4

theorem mem_extended_iff (x : L) : x ∈ I.extended L hf ↔ x ∈ span B (map_f '' I) := by
  constructor <;>
    { intro hx; simpa
    }

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru