pow_dvd_pow_of_add_pow_eq_zero — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem pow_dvd_pow_of_add_pow_eq_zero (hp : n + m ≤ p + 1) (h_comm : Commute x y) (h : (x + y) ^ n = 0) :
    x ^ m ∣ y ^ p := by
  rw [← neg_neg y, neg_pow']
  apply dvd_mul_of_dvd_left
  apply h_comm.neg_right.pow_dvd_pow_of_sub_pow_eq_zero hp
  simpa

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