Documentation

TauCeti.Algebra.Ring.NegOnePow

Powers of negative one in a ground ring #

This file provides the cast to a ground ring of Mathlib's unit-valued sign character Int.negOnePow : ℤ → ℤˣ; the cast factors through ℤ.

Main definitions #

Main results #

source
def TauCeti.negOnePowCast (R : Type uR) [Ring R] (e : ℤ) :
R

The scalar (-1) ^ e in a ground ring.

Equations
Instances For
    source
    theorem TauCeti.negOnePowCast_eq_intCast {R : Type uR} [Ring R] (e : ℤ) :
    negOnePowCast R e = ↑↑e.negOnePow

    The ground-ring sign is the cast of Mathlib's Int.negOnePow.

    source
    @[simp]
    theorem TauCeti.negOnePowCast_zero {R : Type uR} [Ring R] :
    negOnePowCast R 0 = 1
    source
    @[simp]
    theorem TauCeti.negOnePowCast_one {R : Type uR} [Ring R] :
    negOnePowCast R 1 = -1
    source
    @[simp]
    theorem TauCeti.negOnePowCast_neg {R : Type uR} [Ring R] (a : ℤ) :
    negOnePowCast R (-a) = negOnePowCast R a
    source
    theorem TauCeti.negOnePowCast_add {R : Type uR} [Ring R] (a b : ℤ) :
    negOnePowCast R (a + b) = negOnePowCast R a * negOnePowCast R b
    source
    @[simp]
    theorem TauCeti.negOnePowCast_two_mul {R : Type uR} [Ring R] (a : ℤ) :
    negOnePowCast R (2 * a) = 1
    source
    theorem TauCeti.negOnePowCast_even {R : Type uR} [Ring R] {e : ℤ} (he : Even e) :
    negOnePowCast R e = 1
    source
    theorem TauCeti.negOnePowCast_odd {R : Type uR} [Ring R] {e : ℤ} (he : Odd e) :
    negOnePowCast R e = -1
    source
    theorem TauCeti.negOnePow_smul_eq_negOnePowCast_smul {R : Type uR} [Ring R] {A : Type uA} [AddCommGroup A] [Module R A] (e : ℤ) (a : A) :
    e.negOnePow • a = negOnePowCast R e • a

    A sign (-1) ^ e, acting through the units of ℤ, acts as its cast to the ground ring.

    source
    @[simp]
    theorem TauCeti.negOnePowCast_smul_negOnePowCast_smul {R : Type uR} [Ring R] {A : Type uA} [MulAction R A] (e : ℤ) (a : A) :
    negOnePowCast R e • negOnePowCast R e • a = a

    The scalar (-1) ^ e acts as an involution.

    source
    @[simp]
    theorem TauCeti.negOnePowCast_smul_eq_zero_iff {R : Type uR} [Ring R] {A : Type uA} [AddMonoid A] [DistribMulAction R A] (e : ℤ) (a : A) :
    negOnePowCast R e • a = 0 ↔ a = 0
    source
    @[simp]
    theorem TauCeti.negOnePow_smul_negOnePow_smul {A : Type uA} [AddGroup A] (e : ℤ) (a : A) :
    e.negOnePow • e.negOnePow • a = a

    The sign (-1) ^ e, acting through the units of ℤ, acts as an involution.

    source
    theorem TauCeti.negOnePowCast_sum {R : Type uR} [CommRing R] {ι : Type uI} (s : Finset ι) (f : ι → ℤ) :
    negOnePowCast R (∑ i ∈ s, f i) = ∏ i ∈ s, negOnePowCast R (f i)

    The sign of a finite sum is the product of the signs of its terms: the sign character turns addition into multiplication, so it distributes over Finset.sum.