det_fderivPiPolarCoordSymm — Mathlib

English

The determinant of the derivative of the Pi-polarSymm map equals the product of the radii: det fderivPiPolarCoordSymm(p) = ∏_i (p_i)_1.

Русский

Определитель производной полярной симм-получателя равен произведению радиусов: det fderivPiPolarCoordSymm(p) = ∏_i (p_i)_1.

LaTeX

$$$(fderivPiPolarCoordSymm(p)).\mathrm{det} = \prod_i (p_i)_1.$$$

Lean4

theorem det_fderivPiPolarCoordSymm (p : ι → ℝ × ℝ) : (fderivPiPolarCoordSymm p).det = ∏ i, (p i).1 := by
  simp_rw [fderivPiPolarCoordSymm, ContinuousLinearMap.det_pi, det_fderivPolarCoordSymm]

Похожие утверждения