ker

Mathlib.Algebra.Module.Submodule.Ker

URI: https://scilib.ai/kg/mathlib#LinearEquiv.ker

English

For a linear map l and a linear equivalence e'', the kernel of the composed map e'' ∘ l equals the kernel of l.

Русский

Для линейного отображения l и линейного эквивалента e'' ядро e'' ∘ l равно ядру l.

LaTeX

$$$\ker((e''\circ l)) = \ker l$$$

Lean4

@[simp]
protected theorem ker : LinearMap.ker (e : M →ₛₗ[σ₁₂] M₂) = ⊥ :=
  LinearMap.ker_eq_bot_of_injective e.toEquiv.injective

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

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

Разделы

Аффилиация

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