symm — Mathlib

English

If (h,e,f) forms an sl2-triple, then (-h,f,e) also forms an sl2-triple.

Русский

Если (h,e,f) образуют тройку sl2, то (-h,f,e) также образуют sl2-тройку.

LaTeX

$$IsSl2Triple h e f implies IsSl2Triple (-h) f e.$$

Lean4

theorem symm (ht : IsSl2Triple h e f) : IsSl2Triple (-h) f e
    where
  h_ne_zero := by simpa using ht.h_ne_zero
  lie_e_f := by rw [← neg_eq_iff_eq_neg, lie_skew, ht.lie_e_f]
  lie_h_e_nsmul := by rw [neg_lie, neg_eq_iff_eq_neg, ht.lie_h_f_nsmul]
  lie_h_f_nsmul := by rw [neg_lie, neg_inj, ht.lie_h_e_nsmul]

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