English
Equivalent determinant expression for finrank(K) times regOfFamily u via two equivalent forms of the matrix built from logs.
Русский
Эквивалентное выражение через det для произведения finrank(K) на regOfFamily u через две формы матрицы логарифмов.
LaTeX
$$$\\text{Equivalent form: } finrank(K) \\cdot regOfFamily u = |\\det(\\text{matrix of logs with cases on } i) |$$$
Lean4
/-- For any infinite place `w'`, the regulator of the family `u` is equal to the absolute value of
the determinant of the matrix with entries `(mult w * log w (u i))_i` for `w ≠ w'`.
-/
theorem regOfFamily_eq_det (u : Fin (rank K) → (𝓞 K)ˣ) (w' : InfinitePlace K) (e : { w // w ≠ w' } ≃ Fin (rank K)) :
regOfFamily u = |(of fun i w : { w // w ≠ w' } ↦ (mult w.val : ℝ) * Real.log (w.val (u (e i) : K))).det| := by
simp [regOfFamily_eq_det', abs_det_eq_abs_det u e (equivFinRank K).symm, logEmbedding]
