ker_equiv_comp

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#RingHom.ker_equiv_comp

← MathLib Explorer

English

If e is a ring equivalence, then ker (e ∘ f) = ker f.

Русский

Если e — кольцевой эквивалент, то ker (e ∘ f) = ker f.

LaTeX

$$$\\ker (e^{\\mathrm{toRingHom}} \\circ f) = \\ker f$$$

Lean4

theorem ker_equiv_comp (f : R →+* S) (e : S ≃+* T) : ker (e.toRingHom.comp f) = RingHom.ker f := by
  rw [← RingHom.comap_ker, RingEquiv.toRingHom_eq_coe, RingHom.ker_coe_equiv, RingHom.ker]

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

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

Разделы

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

Аффилиация

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