regOfFamily_eq_zero — Mathlib

English

If the family u has maximal rank, regOfFamily u equals the covolume of the Z-span of the basis of IsMaxRank, i.e., regOfFamily u is the regulator computed from the fundSystem basis.

Русский

Если семейство u имеет максимальный ранг, то regOfFamily u равен ковольюму Z-замыкания базиса IsMaxRank; т.е. регулятор равен регулятору, полученному из базиса fundSystem.

LaTeX

$$$\\text{regOfFamily }u = Z\\!Lattice.covolume(\\operatorname{span}_{\\mathbb{Z}}(\\{\\text{basisOfIsMaxRank }hu_i\\}))$$$

Lean4

theorem regOfFamily_eq_zero {u : Fin (rank K) → (𝓞 K)ˣ} (hu : ¬IsMaxRank u) : regOfFamily u = 0 := by
  rw [regOfFamily, dif_neg hu]

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