add_pow_add_pred_mem_of_pow_mem_of_commute

English

If ha: a^m ∈ I and hb: b^n ∈ I and a,b commute, then (a+b)^(m+n-1) ∈ I.

Русский

Если ha: a^m ∈ I и hb: b^n ∈ I и a, b commute, то (a+b)^(m+n-1) ∈ I.

LaTeX

$$Given ha, hb and commutativity, then (a+b)^(m+n-1) ∈ I.$$

Lean4

theorem add_pow_add_pred_mem_of_pow_mem_of_commute {m n : ℕ} (ha : a ^ m ∈ I) (hb : b ^ n ∈ I) (hab : Commute a b) :
    (a + b) ^ (m + n - 1) ∈ I :=
  I.add_pow_mem_of_pow_mem_of_le_of_commute ha hb (by rw [← Nat.sub_le_iff_le_add]) hab

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