isNilpotent_f — Mathlib

English

For i ≠ j, [e_i, f_j] = 0 under crystallographic and reduced/irreducible assumptions.

Русский

Для i ≠ j, при кристаллографических и редукционных/неразложимых предположениях, [e_i, f_j] = 0.

LaTeX

$$$[e_i, f_j] = 0 \\quad \\text{for } i \\neq j$$$

Lean4

theorem isNilpotent_f : IsNilpotent (f i) :=
  by
  obtain ⟨n, hn⟩ := isNilpotent_e i
  suffices (ω b) * (f i ^ n) = 0 from ⟨n, by simpa [← mul_assoc] using congr_arg (ω b * ·) this⟩
  suffices (ω b) * (f i ^ n) = (e i ^ n) * (ω b) by simp [this, hn]
  clear hn
  induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]

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