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]