coe_extended_eq_span

Mathlib.RingTheory.FractionalIdeal.Extended

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

English

The extended equals the span in a simp-friendly form.

Русский

Расширение эквивалентно span в упрощающей форме.

LaTeX

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

Lean4

@[simp]
theorem coe_extended_eq_span : I.extended L hf = span B (map_f '' I) := by ext; simp [mem_coe, mem_extended_iff]

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

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

Разделы

Аффилиация

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