map_coeIdeal

Mathlib.RingTheory.FractionalIdeal.Operations

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

English

Another formulation: the map of an ideal I by g equals the ideal I when viewed in fractional form.

Русский

Еще одно формулирование: образ идеала I по g равен I при виде дробного идеала.

LaTeX

$$FractionalIdeal.map g (FractionalIdeal.coeIdeal I) = FractionalIdeal.coeIdeal I$$

Lean4

@[simp, norm_cast]
theorem map_coeIdeal (I : Ideal R) : (I : FractionalIdeal S P).map g = I :=
  by
  ext x
  simp

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

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

Разделы

Аффилиация

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