exact_iff

Mathlib.Algebra.Exact

URI: https://scilib.ai/kg/mathlib#AddMonoidHom.exact_iff

English

For additive groups, exactness of f,g is equivalent to ker g = range f.

Русский

Для аддитивных групп точность f,g эквивалентна равенству ядер и образа: ker g = range f.

LaTeX

$$$\\mathrm{Exact}(f,g) \\iff \\ker g = \\mathrm{range} f$$

Lean4

theorem exact_iff : Exact f g ↔ ker g = range f :=
  Iff.symm SetLike.ext_iff

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

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

Разделы

Аффилиация

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