coeIdeal_top

Mathlib.RingTheory.FractionalIdeal.Basic

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

English

The top ideal of R, viewed as a fractional ideal, corresponds to the unit element in FractionalIdeal S P.

Русский

Верхний идеал числа R, рассмотренный как дробный идеал, соответствует единице в FractionalIdeal S P.

LaTeX

$$$((\top : \mathrm{Ideal} R) : \mathrm{FractionalIdeal} S P) = 1$$$

Lean4

@[simp, norm_cast]
theorem coeIdeal_top : ((⊤ : Ideal R) : FractionalIdeal S P) = 1 :=
  rfl

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

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

Разделы

Аффилиация

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