linearMap_ker_eq

Mathlib.Algebra.Exact

URI: https://scilib.ai/kg/mathlib#Function.Exact.linearMap_ker_eq

English

If f: M → N and g: N → P are exact, then ker(g) = ran(f).

Русский

Если f: M → N и g: N → P образуют точную последовательность, тогда ker(g) = ran(f).

LaTeX

$$$$ \\ker g = \\operatorname{ran} f. $$$$

Lean4

theorem linearMap_ker_eq (hfg : Exact f g) : ker g = range f :=
  SetLike.ext hfg

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

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

Разделы

Аффилиация

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