add_pow_add_eq_zero_of_pow_eq_zero

English

If x and y commute and x^m = 0, y^n = 0, then (x+y)^{m+n-1} = 0.

Русский

Если x и y коммутируют и x^m = 0, y^n = 0, то (x+y)^{m+n-1} = 0.

LaTeX

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

Lean4

theorem add_pow_add_eq_zero_of_pow_eq_zero (h_comm : Commute x y) {m n : ℕ} (hx : x ^ m = 0) (hy : y ^ n = 0) :
    (x + y) ^ (m + n - 1) = 0 :=
  h_comm.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero hx hy <| by rw [← Nat.sub_le_iff_le_add]

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