WittVector.one_coeff_zero
theorem WittVector.one_coeff_zero :
β (p : β) (R : Type u_1) [hp : Fact p.Prime] [inst : CommRing R], WittVector.coeff 1 0 = 1
The theorem `WittVector.one_coeff_zero` states that for any natural number `p` and any type `R` such that `p` is a prime number (as defined by `Nat.Prime p`) and `R` is a commutative ring (as defined by `CommRing R`), the coefficient of the `0`th term in the Witt vector representation of the number `1` is `1`. In other words, the 0-th coefficient of `1` in the Witt vector space over a commutative ring is always `1`, regardless of the prime number used to define the Witt vector.
More concisely: For any prime number $p$ and commutative ring $R$, the 0-th coefficient of the Witt vector representation of $1$ is $1$.
|
WittVector.one_coeff_eq_of_pos
theorem WittVector.one_coeff_eq_of_pos :
β (p : β) (R : Type u_1) [hp : Fact p.Prime] [inst : CommRing R] (n : β), 0 < n β WittVector.coeff 1 n = 0 := by
sorry
The theorem `WittVector.one_coeff_eq_of_pos` states that for any natural number `p`, any type `R` with a commutative ring structure, and any natural number `n` where `n > 0` and `p` is a prime number, the `n-th` coefficient of the number `1` in the Witt vector ring over `R` with respect to the prime `p`, is `0`. Hence, apart from the zeroth coefficient, all other coefficients of `1` in the Witt vector representation are `0`.
More concisely: For any prime number `p` and natural number `n > 0` in a commutative ring `R`, the `n-th` coefficient of `1` in its Witt vector representation is `0`.
|
WittVector.zero_coeff
theorem WittVector.zero_coeff :
β (p : β) (R : Type u_1) [hp : Fact p.Prime] [inst : CommRing R] (n : β), WittVector.coeff 0 n = 0
The theorem `WittVector.zero_coeff` states that for every natural number `p`, a mathematical object of type `R` (where `R` is a commutative ring), and another natural number `n`, if `p` is a prime number, then the `n`-th coefficient of the zero Witt vector is zero. In other words, this theorem tells us that the coefficients of the zero vector in the Witt vector space over a commutative ring are all zeroes, regardless of the prime number used to define the Witt vector space.
More concisely: For every prime number `p` and commutative ring `R`, the `n`-th coefficient of the zero Witt vector over `R` is zero.
|
WittVector.ext
theorem WittVector.ext : β {p : β} {R : Type u_1} {x y : WittVector p R}, (β (n : β), x.coeff n = y.coeff n) β x = y
The theorem `WittVector.ext` states that for any prime number `p`, any type `R`, and any two Witt vectors `x` and `y` over `R` with coefficients in the natural numbers, if the coefficients of `x` and `y` are equal for all natural numbers, then `x` and `y` are the same Witt vector. In more mathematical terms, this theorem asserts the uniqueness of Witt vectors: two Witt vectors are equal if and only if their coefficients are equal for all indices in the set of natural numbers.
More concisely: Given any prime number `p` and types `R` and `W` for Witt vectors over `R` with coefficients in the natural numbers, two Witt vectors `x` and `y` over `R` are equal if and only if their corresponding coefficient sequences are equal.
|
WittVector.v2_coeff
theorem WittVector.v2_coeff :
β {p' : β} {R' : Type u_2} (x y : WittVector p' R') (i : Fin 2), (![x, y] i).coeff = ![x.coeff, y.coeff] i := by
sorry
This theorem states that for any natural number `p'` and any type `R'`, and for any two Witt vectors `x` and `y` over these, the `.coeff` method applied to the `i`'th element (where `i` is a value in the finite set of size 2) of the vector containing `x` and `y` equals the `i`'th element of the vector formed by the `.coeff` methods of `x` and `y`. In other words, the theorem asserts that taking the `i`'th element and then the coefficient is the same as first taking the coefficient and then the `i`'th element.
More concisely: For any natural number `p` and type `R`, and for any Witt vectors `x` and `y` over `R` of length 2, the `i`-th coefficient of the vector containing `x.coeff i` and `y.coeff i` is equal to `x.coeff i.coeff p` and `y.coeff i.coeff p`.
|