trivial_iff_lower_central_eq_bot — Mathlib

English

IsTrivial L M is equivalent to the first lower central series being zero.

Русский

IsTrivial L M эквивалентно тому, что γ_1 = ⊥.

LaTeX

$$$IsTrivial(L,M) \\iff lowerCentralSeries(R,L,M,1) = ⊥$$$

Lean4

theorem trivial_iff_lower_central_eq_bot : IsTrivial L M ↔ lowerCentralSeries R L M 1 = ⊥ :=
  by
  constructor <;> intro h
  · simp
  · rw [LieSubmodule.eq_bot_iff] at h; apply IsTrivial.mk; intro x m; apply h
    apply LieSubmodule.subset_lieSpan
    simp only [Subtype.exists, LieSubmodule.mem_top, exists_prop, true_and, Set.mem_setOf]
    exact ⟨x, m, rfl⟩

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