ω_mul_f — Mathlib

English

The matrix ω intertwines f and e via the relation ω f = e ω, reflecting the sl2-triple symmetry between the raising and lowering operators.

Русский

Матрица ω связывает f и e через соотношение ω f = e ω, отражая симметрию между операторами подъёма и спуска в тройке sl2.

LaTeX

$$$\omega(b) f(i) = e(i) \omega(b)$ for all i$$

Lean4

theorem ω_mul_f [Fintype ι] (i : b.support) : ω b * f i = e i * ω b := by
  classical
  have := congr_arg (· * ω b) (congr_arg (ω b * ·) (ω_mul_e i))
  simp only [← mul_assoc, ω_mul_ω] at this
  simpa [mul_assoc, ω_mul_ω] using this.symm

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