le_killingCompl_top_of_isLieAbelian

English

If I is Abelian, then I ≤ killingCompl R L ⊤ (repetition of 18536).

Русский

Если I абелева, то I ≤ killingCompl R L ⊤ (повторение 18536).

LaTeX

$$I ≤ LieIdeal.killingCompl R L ⊤$$

Lean4

@[simp]
theorem le_killingCompl_top_of_isLieAbelian [IsLieAbelian I] : I ≤ LieIdeal.killingCompl R L ⊤ :=
  by
  intro x (hx : x ∈ I)
  simp only [mem_killingCompl, LieSubmodule.mem_top, forall_true_left]
  intro y
  rw [LieModule.traceForm_apply_apply]
  exact LieSubmodule.traceForm_eq_zero_of_isTrivial I I (by simp) _ hx

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