coeSubmodule_mono

Mathlib.RingTheory.Localization.Submodule

URI: https://scilib.ai/kg/mathlib#IsLocalization.coeSubmodule_mono

English

If I ≤ J are ideals of R, then the images satisfy coeSubmodule(S,I) ≤ coeSubmodule(S,J).

Русский

Если I ≤ J — идеалы кольца R, то образы удовлетворяют coeSubmodule(S,I) ≤ coeSubmodule(S,J).

LaTeX

$$coeSubmodule_mono h : I ≤ J → coeSubmodule S I ≤ coeSubmodule S J$$

Lean4

theorem coeSubmodule_mono {I J : Ideal R} (h : I ≤ J) : coeSubmodule S I ≤ coeSubmodule S J :=
  Submodule.map_mono h

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

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

Разделы

Аффилиация

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