coeIdeal_bot

Mathlib.RingTheory.FractionalIdeal.Basic

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

English

There is a canonical coercion from ideals to fractional ideals, I ↦ coeIdeal I.

Русский

Существует каноническое преобразование из идеалов в дробные идеалы: I ↦ coeIdeal I.

LaTeX

$$coeIdeal : \mathrm{Ideal}\ R \to \mathrm{FractionalIdeal}\ S\ P$$

Lean4

@[simp, norm_cast]
theorem coeIdeal_bot : ((⊥ : Ideal R) : FractionalIdeal S P) = 0 :=
  rfl

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

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

Разделы

Аффилиация

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