instIsTrivialOfSubsingleton — Mathlib

English

If L is a Lie ring and M is an additive group with a Lie module structure, and L is subsingleton, then the action is trivial.

Русский

Если L — подмножество, тогда действие тривиально.

LaTeX

$$LieModule.IsTrivial L M$$

Lean4

instance instIsTrivialOfSubsingleton {L M : Type*} [LieRing L] [AddCommGroup M] [LieRingModule L M] [Subsingleton L] :
    LieModule.IsTrivial L M :=
  ⟨fun x m ↦ by rw [Subsingleton.eq_zero x, zero_lie]⟩

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