regOfFamily_ne_zero_iff — Mathlib

English

For any infinite place w', regOfFamily u equals the absolute determinant of a matrix whose columns are (mult w · log w (u_i))_i for w ≠ w'.

Русский

Для любого бесконечного места w' регулятор регOfFamily u равен модулю детерминанта матрицы, столбцы которой состоят из (mult w · log w (u_i)) при w ≠ w'.

LaTeX

$$$regOfFamily u = \\left|\\det\\Big( i \\mapsto (mult w).(\\log w (u_i)) \\Big)\\Big|$$$

Lean4

theorem regOfFamily_ne_zero_iff {u : Fin (rank K) → (𝓞 K)ˣ} : regOfFamily u ≠ 0 ↔ IsMaxRank u :=
  ⟨by simpa using (fun hu ↦ regOfFamily_eq_zero hu).mt, fun hu ↦ regOfFamily_ne_zero hu⟩

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