Powers of x + y for a square-zero element x

In any semiring, if x * x = 0 and x commutes with y, then only the terms of degree at most one in x survive in the binomial expansion: (x + y) ^ (n + 1) = y ^ (n + 1) + (n + 1) • (x * y ^ n). In particular an element x with x ^ 2 = 0 satisfies (1 + x) ^ n = 1 + n • x. Hence, in a ring, 1 + x has order dividing n only when n • x = 0, so x = 0 whenever n is invertible. For an endomorphism 1 + N with N ∘ N = 0, this says that a unipotent element of order invertible in the base field is the identity.

Main results

• Commute.add_pow_succ_of_mul_self_eq_zero: if x commutes with y and x * x = 0, then (x + y) ^ (n + 1) = y ^ (n + 1) + (n + 1) • (x * y ^ n).
• TauCeti.one_add_pow_of_sq_eq_zero: (1 + x) ^ n = 1 + n • x when x ^ 2 = 0.
• TauCeti.eq_zero_of_one_add_pow_eq_one_of_sq_eq_zero: if x ^ 2 = 0, (1 + x) ^ n = 1 and n is a unit, then x = 0.

theorem Commute.add_pow_succ_of_mul_self_eq_zero {A : Type u_1} [Semiring A] {x y : A} (h : Commute x y) (hx : x * x = 0) (n : ℕ) : (x + y) ^ (n + 1) = y ^ (n + 1) + (n + 1) • (x * y ^ n)

If x commutes with y and x * x = 0, then only the terms of degree at most one in x survive in the binomial expansion of (x + y) ^ (n + 1).

theorem TauCeti.one_add_pow_of_sq_eq_zero {A : Type u_1} [Semiring A] {x : A} (hx : x ^ 2 = 0) (n : ℕ) : (1 + x) ^ n = 1 + n • x

If x ^ 2 = 0, then (1 + x) ^ n = 1 + n • x.

theorem TauCeti.eq_zero_of_one_add_pow_eq_one_of_sq_eq_zero {A : Type u_1} [Ring A] {x : A} (hx : x ^ 2 = 0) {n : ℕ} (hn : IsUnit ↑n) (h : (1 + x) ^ n = 1) : x = 0

If x ^ 2 = 0 and (1 + x) ^ n = 1 for some n invertible in A, then x = 0.