English
A duplicate of the zeroth-coefficient multiplication law: the zeroth coefficient of the product equals the product of zeroth coefficients.
Русский
Повторение правила: нулевой коэффициент произведения равен произведению нулевых коэффициентов.
LaTeX
$$$(x\cdot y).\text{coeff } 0 = x.\text{coeff } 0 \cdot y.\text{coeff } 0$$$
Lean4
/-- Upgrade a Witt vector `A` whose first entry `A.coeff 0` is a unit to be, itself, a unit in `𝕎 k`.
-/
def mkUnit {a : Units k} {A : 𝕎 k} (hA : A.coeff 0 = a) : Units (𝕎 k) :=
Units.mkOfMulEqOne A (@WittVector.mk' p _ (inverseCoeff a A))
(by
ext n
induction n with
| zero => simp [WittVector.mul_coeff_zero, inverseCoeff, hA]
| succ n => ?_
let H_coeff :=
A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) +
nthRemainder p n (truncateFun (n + 1) A) fun i : Fin (n + 1) => inverseCoeff a A i
have H := Units.mul_inv (a ^ p ^ (n + 1))
linear_combination (norm := skip) -H_coeff * H
have ha : (a : k) ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1)) := by norm_cast
have ha_inv : (↑a⁻¹ : k) ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹ := by norm_cast
simp only [nthRemainder_spec, inverseCoeff, succNthValUnits, hA, one_coeff_eq_of_pos, Nat.succ_pos', ha_inv, ha,
inv_pow]
ring!)
