English
The determinant of the derivative of polarCoord.symm at p equals the radial coordinate r, i.e., det D(p) = p_1.
Русский
Определитель производной polarCoord.symm в точке p равен радиальной координате: det D(p) = p_1.
LaTeX
$$$$ \det\big( D(\mathrm{polarCoord.symm})(p) \big) = p_1. $$$$
Lean4
theorem hasFDerivAt_polarCoord_symm (p : ℝ × ℝ) : HasFDerivAt polarCoord.symm (fderivPolarCoordSymm p) p :=
by
unfold fderivPolarCoordSymm
rw [Matrix.toLin_finTwoProd_toContinuousLinearMap]
convert
HasFDerivAt.prodMk (𝕜 := ℝ) (hasFDerivAt_fst.mul ((hasDerivAt_cos p.2).comp_hasFDerivAt p hasFDerivAt_snd))
(hasFDerivAt_fst.mul ((hasDerivAt_sin p.2).comp_hasFDerivAt p hasFDerivAt_snd)) using
2 <;>
simp [smul_smul, add_comm, neg_mul, smul_neg, neg_smul _ (ContinuousLinearMap.snd ℝ ℝ ℝ)]
