pow_dvd_sub_pow_of_pow_eq_zero_left

English

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

Русский

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

LaTeX

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

Lean4

theorem pow_dvd_sub_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 := by
  rw [← neg_sub y x, neg_pow']
  apply dvd_mul_of_dvd_left
  exact h_comm.symm.pow_dvd_sub_pow_of_pow_eq_zero_right hp hx

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