add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero

English

If x and y commute, and x^m = 0, y^n = 0, then (x+y)^{k} = 0 for suitable k when m+n ≤ k+1.

Русский

Если x и y коммутируют и x^m = 0, y^n = 0, тогда (x+y)^k = 0 при подходящем k с условием m+n ≤ k+1.

LaTeX

$$$\\text{Commute}(x,y) \\Rightarrow \\forall m,n,k,\\ x^m=0,\\ y^n=0 \\land m+n \\le k+1 \\Rightarrow (x+y)^k=0$$$

Lean4

theorem add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero (h_comm : Commute x y) {m n k : ℕ} (hx : x ^ m = 0)
    (hy : y ^ n = 0) (h : m + n ≤ k + 1) : (x + y) ^ k = 0 :=
  by
  rw [h_comm.add_pow']
  apply Finset.sum_eq_zero
  rintro ⟨i, j⟩ hij
  suffices x ^ i * y ^ j = 0 by simp only [this, nsmul_eq_mul, mul_zero]
  by_cases hi : m ≤ i
  · rw [pow_eq_zero_of_le hi hx, zero_mul]
  rw [pow_eq_zero_of_le ?_ hy, mul_zero]
  linarith [Finset.mem_antidiagonal.mp hij]

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