add_pow_mem_of_pow_mem_of_le_of_commute

English

If a^m ∈ I and b^n ∈ I and a and b commute, then (a+b)^k ∈ I whenever m+n ≤ k+1.

Русский

Если a^m и b^n принадлежат I и a и b коммутируют, тогда (a+b)^k ∈ I при m+n ≤ k+1.

LaTeX

$$$a^m \\in I,\\; b^n \\in I,\\; a b = b a \\Rightarrow (a+b)^k \\in I \\text{ при } m+n \\le k+1$$$

Lean4

theorem add_pow_mem_of_pow_mem_of_le_of_commute {m n k : ℕ} (ha : a ^ m ∈ I) (hb : b ^ n ∈ I) (hk : m + n ≤ k + 1)
    (hab : Commute a b) : (a + b) ^ k ∈ I :=
  by
  simp_rw [hab.add_pow, ← Nat.cast_comm]
  apply I.sum_mem
  intro c _
  apply mul_mem_left
  by_cases h : m ≤ c
  · rw [hab.pow_pow]
    exact I.mul_mem_left _ (I.pow_mem_of_pow_mem ha h)
  · refine I.mul_mem_left _ (I.pow_mem_of_pow_mem hb ?_)
    cutsat

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