English
Let R be a commutative ring and n a natural number. The determinant of the linear map underlying the Taylor linearization map at r of order n is equal to 1.
Русский
Пусть R — коммутативный кольцо, n — натуральное число. Детерминант линейного отображения, соответствующего линейному отображению Тейлора порядка n, равен 1.
LaTeX
$$$\det\bigl((taylorLinearEquiv\, r\, n).toLinearMap\bigr) = 1$$$
Lean4
@[simp]
theorem det_taylorLinearEquiv_toLinearMap : (taylorLinearEquiv r n).toLinearMap.det = 1 :=
by
nontriviality R
rw [← LinearMap.det_toMatrix (degreeLT.basis R n), Matrix.det_of_upperTriangular, Fintype.prod_eq_one]
· intro i
rw [LinearMap.toMatrix_apply, degreeLT.basis_repr, ← natDegree_X_pow (R := R) (i : ℕ)]
change (taylor r (degreeLT.basis R n i)).coeff _ = 1
rw [degreeLT.basis_val, coeff_taylor_natDegree, leadingCoeff_X_pow]
· intro i j hji
rw [LinearMap.toMatrix_apply, LinearEquiv.coe_coe, degreeLT.basis_repr]
change (taylor r (degreeLT.basis R n j)).coeff i = 0
rw [degreeLT.basis_val, coeff_eq_zero_of_degree_lt (by simpa [-taylor_X_pow, -taylor_pow])]
