add_pow_dvd_pow_of_pow_eq_zero_right

English

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

Русский

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

LaTeX

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

Lean4

theorem add_pow_dvd_pow_of_pow_eq_zero_right (hp : n + m ≤ p + 1) (h_comm : Commute x y) (hx : x ^ n = 0) :
    (x + y) ^ m ∣ y ^ p :=
  (h_comm.add_left rfl).pow_dvd_pow_of_sub_pow_eq_zero hp (by simpa)

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