English
Let u be a unit in R[X]. Then for every n, the coefficient at n of u⁻¹ is the inverse of the coefficient at n of u.
Русский
Пусть u — единица в R[X]. Тогда для каждого n коэффициент у⁻¹ на позиции n равен обратному коэффициенту u на позиции n.
LaTeX
$$$ ((\uparrow u : R[X]).coeff\ n)^{-1} = ((\uparrow u^{-1} : R[X]).coeff\ n) $$$
Lean4
theorem coeff_inv_units (u : R[X]ˣ) (n : ℕ) : ((↑u : R[X]).coeff n)⁻¹ = (↑u⁻¹ : R[X]).coeff n :=
by
rw [eq_C_of_degree_eq_zero (degree_coe_units u), eq_C_of_degree_eq_zero (degree_coe_units u⁻¹), coeff_C, coeff_C,
inv_eq_one_div]
split_ifs
· rw [div_eq_iff_mul_eq (coeff_coe_units_zero_ne_zero u), coeff_zero_eq_eval_zero, coeff_zero_eq_eval_zero, ←
eval_mul, ← Units.val_mul, inv_mul_cancel]
simp
· simp
