exact_of_comp_eq_zero_of_ker_le_range

Mathlib.Algebra.Exact

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

← MathLib Explorer

English

If g ∘ f = 0 and ker g ≤ range f, then Exact f g.

Русский

Если g ∘ f = 0 и ker g ≤ range f, то Exact f g.

LaTeX

$$$(g \\circ f) = 0 \\land \\ker g \\le \\mathrm{range} f \\Rightarrow \\mathrm{Exact}(f,g)$$

Lean4

theorem exact_of_comp_eq_zero_of_ker_le_range (h1 : g ∘ₗ f = 0) (h2 : ker g ≤ range f) : Exact f g :=
  Exact.of_comp_of_mem_range (congrArg DFunLike.coe h1) h2

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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