coe_zero

Mathlib.RingTheory.FractionalIdeal.Basic

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

English

The bottom ideal, viewed as a fractional ideal, equals 0.

Русский

Нижний идеал, рассматриваемый как дробный идеал, равен нулю.

LaTeX

$$((⊥ : Ideal R) : FractionalIdeal S P) = 0$$

Lean4

@[simp, norm_cast]
theorem coe_zero : ↑(0 : FractionalIdeal S P) = (⊥ : Submodule R P) :=
  Submodule.ext fun _ => mem_zero_iff S

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

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

Разделы

Аффилиация

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