English
For any p, n, R, x ∈ 𝕎 R and i ∈ Fin n, the i-th coefficient of the truncated image equals the corresponding coefficient of x: (truncate hm x).coeff i = x.coeff (Fin.castLE hm i).
Русский
Пусть x ∈ 𝕎 R и i ∈ Fin n. Тогда i-й коэффициент усечения x равен соответствующему коэффициенту x: (truncate hm x).coeff i = x.coeff (Fin.castLE hm i).
LaTeX
$$$$ (\\operatorname{truncate} hm\\ x).\\mathrm{coeff} i = x.\\mathrm{coeff} (\\\\Fin.castLE hm i). $$$$
Lean4
@[simp]
theorem coeff_truncate {m : ℕ} (hm : n ≤ m) (i : Fin n) (x : TruncatedWittVector p m R) :
(truncate hm x).coeff i = x.coeff (Fin.castLE hm i) :=
by
obtain ⟨y, rfl⟩ := @WittVector.truncate_surjective p _ _ _ _ x
simp only [truncate_wittVector_truncate, WittVector.coeff_truncate, Fin.coe_castLE]
