instIsFaithfulOfHasTrivialRadical

English

If the radical is trivial, the adjoint action of L on itself is faithful (kernel is zero).

Русский

Если радикал тривиален, то отображение адъюнкта на самом L сохраняет всю информацию, его ядро равно нулю.

LaTeX

$$$(HasTrivialRadical\; R\; L) \Rightarrow LieModule.IsFaithful\; R\; L\; L$$$

Lean4

instance [HasTrivialRadical R L] : LieModule.IsFaithful R L L :=
  by
  rw [isFaithful_self_iff]
  exact HasTrivialRadical.eq_bot_of_isSolvable _

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