English
For x, y in Witt vectors with disjoint support condition (∀ n, x.coeff n = 0 or y.coeff n = 0), (x + y).coeff n = x.coeff n + y.coeff n.
Русский
Для x, y в Witt-векторах с условием раздельной поддержки (∀ n, x.coeff n = 0 или y.coeff n = 0) выполняется (x + y).coeff n = x.coeff n + y.coeff n.
LaTeX
$$$ (x + y).coeff n = x.coeff n + y.coeff n $ при условии $ \forall n, x.coeff n = 0 \lor y.coeff n = 0 $$$
Lean4
theorem coeff_add_of_disjoint (x y : 𝕎 R) (h : ∀ n, x.coeff n = 0 ∨ y.coeff n = 0) :
(x + y).coeff n = x.coeff n + y.coeff n :=
by
let P : ℕ → Prop := fun n => y.coeff n = 0
haveI : DecidablePred P := Classical.decPred P
set z := mk p fun n => if P n then x.coeff n else y.coeff n
have hx : select P z = x := by
ext1 n; rw [select, coeff_mk, coeff_mk]
split_ifs with hn
· rfl
· rw [(h n).resolve_right hn]
have hy : select (fun i => ¬P i) z = y := by
ext1 n; rw [select, coeff_mk, coeff_mk]
split_ifs with hn
· exact hn.symm
· rfl
calc
(x + y).coeff n = z.coeff n := by rw [← hx, ← hy, select_add_select_not P z]
_ = x.coeff n + y.coeff n := by
simp only [z, mk.eq_1]
split_ifs with y0
· rw [y0, add_zero]
· rw [h n |>.resolve_right y0, zero_add]
