mem_killingCompl — Mathlib

English

An element x lies in I.killingCompl iff x is orthogonal to all elements y of I with respect to Killing form; equivalently, killingForm R L y x = 0 for all y ∈ I.

Русский

Элемент x принадлежит I.killingCompl тогда и только тогда, когда он ортогонален всем элементам y∈I по Killing форме; тождественно killingForm R L y x = 0 для всех y∈I.

LaTeX

$${x : L} ∈ I.killingCompl ↔ ∀ y ∈ I, killingForm R L y x = 0$$

Lean4

@[simp]
theorem mem_killingCompl {x : L} : x ∈ I.killingCompl ↔ ∀ y ∈ I, killingForm R L y x = 0 := by rfl

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