lie_comm — Mathlib

English

The bracket [I,N] is zero (i.e., equals the bottom) iff every bracket [x,m] with x ∈ I and m ∈ N is zero.

Русский

Скобка [I,N] равна нулю тогда и только тогда, когда каждое [x,m] с x ∈ I и m ∈ N равно нулю.

LaTeX

$$$$ [I,N] = \{0\} \iff \forall x \in I, \forall m \in N, [x,m] = 0. $$$$

Lean4

theorem lie_comm : ⁅I, J⁆ = ⁅J, I⁆ :=
  by
  suffices ∀ I J : LieIdeal R L, ⁅I, J⁆ ≤ ⁅J, I⁆ by exact le_antisymm (this I J) (this J I)
  clear! I J; intro I J
  rw [lieIdeal_oper_eq_span, lieSpan_le]; rintro x ⟨y, z, h⟩; rw [← h]
  rw [← lie_skew, ← lie_neg, ← LieSubmodule.coe_neg]
  apply lie_coe_mem_lie

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