fderiv_expMapBasis — Mathlib

English

The absolute determinant of fderiv_expMapBasis(x) equals exp(x_{w0} * finrank) times the inverse product of expMapBasis(x) over complex places, times 2^{-nrComplexPlaces} times finrank times regulator.

Русский

Модульdet fderiv_expMapBasis(x) равен exp(x_{w0} * finrank) умножить на обратное произведение expMapBasis(x) по комплексным местам, умноженное на 2^{-nrComplexPlaces} и на regulator поля.

LaTeX

$$|(fderiv_expMapBasis K x).det| = exp(x_{w_0} * \operatorname{finrank} \mathbb{Q} K) \cdot \left(\prod w : { w // IsComplex w }, \expMapBasis x w.1\right)^{-1} \cdot 2^{-\mathrm{nrComplexPlaces} K} \cdot (\operatorname{finrank} \mathbb{Q} K) \cdot \operatorname{regulator} K$$

Lean4

/-- The derivative of `expMapBasis`, see `hasFDerivAt_expMapBasis`.
-/
abbrev fderiv_expMapBasis (x : realSpace K) : realSpace K →L[ℝ] realSpace K :=
  (fderiv_expMap ((completeBasis K).equivFun.symm x)).comp (completeBasis K).equivFunL.symm.toContinuousLinearMap

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