pow_dvd_add_pow_of_pow_eq_zero_right

English

Let x,y ∈ R commute in a semiring. If hp holds and y^n = 0, then x^m ∣ (x + y)^p.

Русский

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

LaTeX

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

Lean4

theorem pow_dvd_add_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 := by
  rw [h_comm.add_pow']
  refine Finset.dvd_sum fun ⟨i, j⟩ hij ↦ ?_
  replace hij : i + j = p := by simpa using hij
  apply dvd_nsmul_of_dvd
  rcases le_or_gt m i with (hi : m ≤ i) | (hi : i + 1 ≤ m)
  · exact dvd_mul_of_dvd_left (pow_dvd_pow x hi) _
  · simp [pow_eq_zero_of_le (by cutsat : n ≤ j) hy]

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