ker_algebraMap_end — Mathlib

English

For a nonzero scalar a ∈ K in a semifield K, the kernel of the endomorphism a where End(K,V) is formed by algebraMap_K(End(K,V)) a is the bottom submodule; i.e., it is zero.

Русский

Пусть a ≠ 0 в полe K; ядро отображения a в End(K,V) равно нулю.

LaTeX

$$ker (algebraMap K (End K V) a) = ⊥$$

Lean4

@[simp]
theorem ker_algebraMap_end (K : Type u) (V : Type v) [Semifield K] [AddCommMonoid V] [Module K V] (a : K) (ha : a ≠ 0) :
    LinearMap.ker ((algebraMap K (End K V)) a) = ⊥ :=
  LinearMap.ker_smul _ _ ha

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