ker_le_ker_comp

Mathlib.Algebra.Module.Submodule.Ker

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

← MathLib Explorer

English

If f: M →ₛₗ M₂ and g: M₂ → M₃ commute, then ker f ⊔ ker g ≤ ker (f ∘ g).

Русский

Если f: M →ₛₗ M₂ и g: M₂ → M₃ commute, то ker f ⊔ ker g ≤ ker(f ∘ g).

LaTeX

$$ker f + ker g ≤ ker (f ∘ g) if Commute f g$$

Lean4

theorem ker_le_ker_comp (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : ker f ≤ ker (g.comp f : M →ₛₗ[τ₁₃] M₃) := by
  rw [ker_comp]; exact comap_mono bot_le

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

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

Разделы

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

Аффилиация

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