coeToSubmodule_inj

Mathlib.RingTheory.FractionalIdeal.Basic

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

English

If a submodule I of P satisfies I ≤ 1, then I is a fractional ideal with respect to S.

Русский

Если подмодуль I удовлетворяет условию I ≤ 1, то I является дробным идеалом относительно S.

LaTeX

$$$I \le 1 \Rightarrow IsFractional\ S\ I$$$

Lean4

theorem coeToSubmodule_inj {I J : FractionalIdeal S P} : (I : Submodule R P) = J ↔ I = J :=
  coeToSubmodule_injective.eq_iff

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

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

Разделы

Аффилиация

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