English
The product of the rational rank of K and regOfFamily u equals the absolute determinant of a matrix built from logs of fundSystem and embeddings, i.e., finrank(K) · regOfFamily u = |det of a suitable matrix|.
Русский
Произведение рационального ранга K на regOfFamily u равно модулю детерминанта матрицы, составленной из логарифмов вложений фундаментальной системы и эмбеддингов.
LaTeX
$$$\\mathrm{finrank}_{\\mathbb{Q}}(K) \\cdot regOfFamily u = \\left|\\det\\Big( \\text{matrix of logs }\\Big)\\right|$$$
Lean4
theorem regOfFamily_eq_det' (u : Fin (rank K) → (𝓞 K)ˣ) :
regOfFamily u = |(of fun i ↦ logEmbedding K (Additive.ofMul (u ((equivFinRank K).symm i)))).det| :=
by
by_cases hu : IsMaxRank u
· rw [regOfFamily_of_isMaxRank hu,
ZLattice.covolume_eq_det _ (((basisOfIsMaxRank hu).restrictScalars ℤ).reindex (equivFinRank K)),
Basis.coe_reindex]
congr 3 with i
simp [basisOfIsMaxRank_apply hu]
· rw [regOfFamily_eq_zero hu, det_eq_zero_of_not_linearIndependent_rows, abs_zero]
rwa [IsMaxRank, ← linearIndependent_equiv (equivFinRank K).symm] at hu
