Parity of exponents of -1, of negated elements, and of nonzero elements

This file records the identity 1 - (-x)^{2n+1} = 1 + x^{2n+1} in a ring, which turns a product of factors 1 - (-q)^{2n+1} into a product of factors 1 + q^{2n+1}, and two sign cancellations for powers of -1 in a monoid with a distributive negation: an even summand of the exponent can be dropped, and two equal powers of -1 cancel. It also records that multiplying a sign ±1 by a power of -1 gives a sign.

Finally, it records that a nonzero even element keeps 2 nonzero: Even.two_ne_zero_of_ne_zero. Combined with Even.intCast, a hypothesis (n : R) ≠ 0 on an even integer n yields (2 : R) ≠ 0.

theorem TauCeti.one_sub_neg_pow_odd {R : Type u_1} [Ring R] (x : R) (n : ℕ) : 1 - (-x) ^ (2 * n + 1) = 1 + x ^ (2 * n + 1)

1 - (-x)^{2n+1} = 1 + x^{2n+1}.

@[simp]

theorem TauCeti.neg_one_pow_add_two_mul {α : Type u_1} [Monoid α] [HasDistribNeg α] (a b : ℕ) : (-1) ^ (a + 2 * b) = (-1) ^ a

An even summand of the exponent of -1 can be dropped: (-1)^{a + 2b} = (-1)^a.

@[simp]

theorem TauCeti.neg_one_pow_mul_neg_one_pow_mul {α : Type u_1} [Monoid α] [HasDistribNeg α] (a : ℕ) (x : α) : (-1) ^ a * ((-1) ^ a * x) = x

Two equal powers of -1 cancel: (-1)^a * ((-1)^a * x) = x.

theorem TauCeti.neg_one_pow_mul_eq_or {α : Type u_1} [Monoid α] [HasDistribNeg α] {μ : α} (hμ : μ = 1 ∨ μ = -1) (n : ℕ) : (-1) ^ n * μ = 1 ∨ (-1) ^ n * μ = -1

Multiplying a sign μ = ±1 by a power of -1 gives a sign.

theorem Even.two_ne_zero_of_ne_zero {R : Type u_1} [NonAssocSemiring R] {x : R} (hx : Even x) (h : x ≠ 0) : 2 ≠ 0

A nonzero even element forces 2 to be nonzero: it is 2 times something, so a vanishing 2 would make it vanish too.