pow_dvd_sub_pow_of_pow_eq_zero_right

English

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

Русский

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

LaTeX

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

Lean4

theorem pow_dvd_sub_pow_of_pow_eq_zero_right (hp : n + m ≤ p + 1) (h_comm : Commute x y) (hy : y ^ n = 0) :
    x ^ m ∣ (x - y) ^ p :=
  (sub_right rfl h_comm).pow_dvd_pow_of_sub_pow_eq_zero hp (by simpa)

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