disjoint_ker

Mathlib.Algebra.Module.Submodule.Ker

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

English

For linear maps f and g, ker f ≤ ker (g ∘ f).

Русский

Для линейных отображений f и g: ker f ≤ ker(g ∘ f).

LaTeX

$$ker f ≤ ker (g ∘ f)$$

Lean4

theorem disjoint_ker {f : F} {p : Submodule R M} : Disjoint p (ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0 := by
  simp [disjoint_def]

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

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

Разделы

Аффилиация

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