addMonoidHom_ker_eq

Mathlib.Algebra.Exact

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

English

If f,g are exact, then ker g = range f.

Русский

Если f и g точны, то ker g = range f.

LaTeX

$$$\\ker g = \\mathrm{range} f$$$

Lean4

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

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

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

Разделы

Аффилиация

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