det_fderivPolarCoordRealSymm — Mathlib

English

The determinant of FDerivPolarCoordRealSymm at x equals the product over complex places of the first component of x.snd w.

Русский

Определитель FDerivPolarCoordRealSymm в x равен произведению по комплексным местам первого компонента x.snd w.

LaTeX

$$$\\bigl(FDerivPolarCoordRealSymm(K)(x)\\bigr).\\det = \\prod_{w : {w // IsComplex w}} (x.2 w).1$$$

Lean4

theorem det_fderivPolarCoordRealSymm (x : realMixedSpace K) :
    (FDerivPolarCoordRealSymm K x).det = ∏ w : { w // IsComplex w }, (x.2 w).1 :=
  by
  have :
    (FDerivPolarCoordRealSymm K x).toLinearMap =
      LinearMap.prodMap (LinearMap.id) (fderivPiPolarCoordSymm x.2).toLinearMap :=
    rfl
  rw [ContinuousLinearMap.det, this, LinearMap.det_prodMap, LinearMap.det_id, one_mul, ← ContinuousLinearMap.det,
    det_fderivPiPolarCoordSymm]

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