English
For Witt vectors x,y and n, the following holds: x and y have equal first n coefficients iff x−y has its first n coefficients equal to zero.
Русский
Для векторов Уитта x,y и натурального n выполняется: совпадают первые n коэффициентов x и y тогда и только тогда, когда разность x−y имеет первые n коэффициентов равными нулю.
LaTeX
$$$$ (\forall i < n,\; x_Coeff(i) = y_Coeff(i)) \;\iff\; (\forall i < n,\; (x - y).coeff_i = 0). $$$$
Lean4
theorem le_coeff_eq_iff_le_sub_coeff_eq_zero {x y : 𝕎 k} {n : ℕ} :
(∀ i < n, x.coeff i = y.coeff i) ↔ ∀ i < n, (x - y).coeff i = 0 := by
calc
_ ↔ x.truncate n = y.truncate n := by
refine ⟨fun h => ?_, fun h i hi => ?_⟩
· ext i
simp [h i]
· rw [← coeff_truncate x ⟨i, hi⟩, ← coeff_truncate y ⟨i, hi⟩, h]
_ ↔ (x - y).truncate n = 0 := by simp only [map_sub, sub_eq_zero]
_ ↔ _ := by simp only [← mem_ker_truncate, RingHom.mem_ker]
