# mathlibdocumentation

ring_theory.witt_vector.init_tail

# init and tail#

Given a Witt vector x, we are sometimes interested in its components before and after an index n. This file defines those operations, proves that init is polynomial, and shows how that polynomial interacts with mv_polynomial.bind₁.

## Main declarations #

• witt_vector.init n x: the first n coefficients of x, as a Witt vector. All coefficients at indices ≥ n are 0.
• witt_vector.tail n x: the complementary part to init. All coefficients at indices < n are 0, otherwise they are the same as in x.
• witt_vector.coeff_add_of_disjoint: if x and y are Witt vectors such that for every n the n-th coefficient of x or of y is 0, then the coefficients of x + y are just x.coeff n + y.coeff n.

## References #

init_ring is an auxiliary tactic that discharges goals factoring init over ring operations.

def witt_vector.select {p : } {R : Type u_1} [comm_ring R] (P : → Prop) (x : R) :
R

witt_vector.select P x, for a predicate P : ℕ → Prop is the Witt vector whose n-th coefficient is x.coeff n if P n is true, and 0 otherwise.

Equations
def witt_vector.select_poly (P : → Prop) (n : ) :

The polynomial that witnesses that witt_vector.select is a polynomial function. select_poly n is X n if P n holds, and 0 otherwise.

Equations
theorem witt_vector.coeff_select {p : } {R : Type u_1} [comm_ring R] (P : → Prop) (x : R) (n : ) :
x).coeff n =
@[instance]
def witt_vector.select_is_poly.comp_i {p : } (P : → Prop) (f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R) [hf : f] :
(λ (R : Type u_1) (_Rcr : , (λ (R : Type u_1) (_Rcr : (x : R), R _Rcr f)
@[instance]
def witt_vector.select_is_poly.comp₂_i {p : } (P : → Prop) (f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R R) [hf : f] :
(λ (R : Type u_1) (_Rcr : (x y : R), (λ (R : Type u_1) (_Rcr : (x : R), R _Rcr (f x y))
theorem witt_vector.select_is_poly {p : } (P : → Prop) :
(λ (R : Type u_1) (_Rcr : (x : R),
theorem witt_vector.select_add_select_not {p : } [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] (P : → Prop) (x : R) :
+ witt_vector.select (λ (i : ), ¬P i) x = x
theorem witt_vector.coeff_add_of_disjoint {p : } [hp : fact (nat.prime p)] (n : ) {R : Type u_1} [comm_ring R] (x y : R) (h : ∀ (n : ), x.coeff n = 0 y.coeff n = 0) :
(x + y).coeff n = x.coeff n + y.coeff n
def witt_vector.init {p : } {R : Type u_1} [comm_ring R] (n : ) :
R R

witt_vector.init n x is the Witt vector of which the first n coefficients are those from x and all other coefficients are 0. See witt_vector.tail for the complementary part.

Equations
def witt_vector.tail {p : } {R : Type u_1} [comm_ring R] (n : ) :
R R

witt_vector.tail n x is the Witt vector of which the first n coefficients are 0 and all other coefficients are those from x. See witt_vector.init for the complementary part.

Equations
@[simp]
theorem witt_vector.init_add_tail {p : } [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] (x : R) (n : ) :
= x
@[simp]
theorem witt_vector.init_init {p : } {R : Type u_1} [comm_ring R] (x : R) (n : ) :
x) =
theorem witt_vector.init_add {p : } [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] (x y : R) (n : ) :
(x + y) = x + y)
theorem witt_vector.init_mul {p : } [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] (x y : R) (n : ) :
(x * y) = x) * y)
theorem witt_vector.init_neg {p : } [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] (x : R) (n : ) :
(-x) =
theorem witt_vector.init_sub {p : } [hp : fact (nat.prime p)] {R : Type u_1} [comm_ring R] (x y : R) (n : ) :
(x - y) = x - y)
theorem witt_vector.init_is_poly (p n : ) :
(λ (R : Type u_1) (_Rcr : ,

witt_vector.init n x is polynomial in the coefficients of x.