toLinearMapLieHom_injective — Mathlib

English

The map toLinearMapLieHom is injective: different Lie Derivations have different associated linear endomorphisms.

Русский

Отображение toLinearMapLieHom инъективно: различные Ли-производные задают различные линейные эндоморфизмы.

LaTeX

$$$\text{toLinearMapLieHom}_\text{inj} : \; (D_1 \neq D_2) \implies (toLinearMapLieHom(D_1) \neq toLinearMapLieHom(D_2))$$$

Lean4

/-- The map from Lie derivations to linear endormophisms is injective. -/
theorem toLinearMapLieHom_injective : Function.Injective (toLinearMapLieHom R L) := fun _ _ h ↦
  ext fun a ↦ congrFun (congrArg DFunLike.coe h) a

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