colon_mono

Mathlib.RingTheory.Ideal.Colon

URI: https://scilib.ai/kg/mathlib#Submodule.colon_mono

← MathLib Explorer

English

If N1 ≤ N2 and P1 ≤ P2 then N1.colon P2 ≤ N2.colon P1.

Русский

Если N1 ≤ N2 и P1 ≤ P2, то N1.colon P2 ≤ N2.colon P1.

LaTeX

$$N1.colon P2 ≤ N2.colon P1$$

Lean4

theorem colon_mono (hn : N₁ ≤ N₂) (hp : P₁ ≤ P₂) : N₁.colon P₂ ≤ N₂.colon P₁ := fun _ hrnp =>
  mem_colon.2 fun p₁ hp₁ => hn <| mem_colon.1 hrnp p₁ <| hp hp₁

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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