pow_dvd_add_pow_of_pow_eq_zero_left

English

If hp holds, x and y commute, and x^n = 0, then y^m ∣ (x+y)^p.

Русский

Если hp выполняется, x и y коммутируют, и x^n = 0, тогда y^m делит (x+y)^p.

LaTeX

$$n + m ≤ p + 1 ∧ Commute(x,y) ∧ x^n = 0 ⇒ y^m \mid (x+y)^p$$

Lean4

theorem pow_dvd_add_pow_of_pow_eq_zero_left (hp : n + m ≤ p + 1) (h_comm : Commute x y) (hx : x ^ n = 0) :
    y ^ m ∣ (x + y) ^ p :=
  add_comm x y ▸ h_comm.symm.pow_dvd_add_pow_of_pow_eq_zero_right hp hx

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