instIsTwoSidedComap

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#Ideal.instIsTwoSidedComap

English

If K is two-sided, then comap f K is two-sided.

Русский

Если K двусторонний, то comap f K также двусторонний.

LaTeX

$$$\text{K.IsTwoSided} \Rightarrow (\operatorname{comap} f K).IsTwoSided$$$

Lean4

instance (priority := low) [K.IsTwoSided] : (comap f K).IsTwoSided :=
  ⟨fun b ha ↦ by rw [mem_comap, map_mul]; exact mul_mem_right _ _ ha⟩

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

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

Разделы

Аффилиация

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