comap_coe

Mathlib.RingTheory.Ideal.Maps

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

English

The same equality as comap with RingHomClass holds for the zero-lift.

Русский

То же равенство, что и для comap с RingHomClass, справедливо и в другой формулировке.

LaTeX

$$$I.\\\\mathrm{comap}(f) = I.\\\\mathrm{comap} (RingHomClass.toRingHom f)$$$

Lean4

theorem comap_coe [RingHomClass F R S] (I : Ideal S) : I.comap (f : R →+* S) = I.comap f :=
  rfl

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

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

Разделы

Аффилиация

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