det_matrixToStdBasis — Mathlib

English

The determinant of the matrixToStdBasis equals (2^{-1} i) raised to the number of complex places.

Русский

Определитель матрицы matrixToStdBasis равен (2^{-1} i) в степени числа комплексных мест.

LaTeX

$$$ \det(\text{matrixToStdBasis } K) = (2^{-1} \cdot i)^{\operatorname{nrComplexPlaces} K} $$$

Lean4

theorem det_matrixToStdBasis : (matrixToStdBasis K).det = (2⁻¹ * I) ^ nrComplexPlaces K :=
  calc
    _ = ∏ _k : { w : InfinitePlace K // IsComplex w }, det ((2 : ℂ)⁻¹ • !![1, 1; -I, I]) := by
      rw [matrixToStdBasis, det_fromBlocks_zero₂₁, det_diagonal, prod_const_one, one_mul, det_reindex_self,
        det_blockDiagonal]
    _ = ∏ _k : { w : InfinitePlace K // IsComplex w }, (2⁻¹ * Complex.I) :=
      by
      refine prod_congr (Eq.refl _) (fun _ _ => ?_)
      simp [field]; ring
    _ = (2⁻¹ * Complex.I) ^ Fintype.card { w : InfinitePlace K // IsComplex w } := by rw [prod_const, Fintype.card]

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