isTrivial_of_nilpotencyLength_le_one

English

If L acts nilpotently on M and nilpotencyLength L M ≤ 1, then L acts trivially on M.

Русский

Если Ли-алгебра действует нильпотентно на M и nilpotencyLength L M ≤ 1, то действие L на M тривиально.

LaTeX

$$$[\\operatorname{IsNilpotent}_L(M)] \\land (\\text{nilpotencyLength}(L,M) \\le 1) \\Rightarrow \\operatorname{IsTrivial}_L(M).$$$

Lean4

theorem isTrivial_of_nilpotencyLength_le_one [IsNilpotent L M] (h : nilpotencyLength L M ≤ 1) : IsTrivial L M :=
  by
  nontriviality M
  rcases Nat.le_one_iff_eq_zero_or_eq_one.mp h with h | h
  · rw [nilpotencyLength_eq_zero_iff] at h; infer_instance
  · rwa [nilpotencyLength_eq_one_iff] at h

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