ker_rangeRestrict

Mathlib.RingTheory.Ideal.Maps

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

English

Restricting the codomain of a map f to its range does not alter its kernel.

Русский

Ограничение области значений отображения f до его образа не меняет его ядро.

LaTeX

$$$\\ker f.rangeRestrict = \\ker f$$$

Lean4

@[simp]
theorem ker_rangeRestrict (f : R →+* S) : ker f.rangeRestrict = ker f :=
  Ideal.ext fun _ ↦ Subtype.ext_iff

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

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

Разделы

Аффилиация

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