exact_iff

Mathlib.Algebra.Exact

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

English

For linear maps between modules, Exact f g iff ker g = range f.

Русский

Для линейных отображений между модулями: Exact f g iff ker g = range f.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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