regOfFamily_of_isMaxRank — Mathlib

English

If the family is of maximal rank, regOfFamily u is strictly positive (and hence nonzero).

Русский

Если семейство единиц имеет максимальный ранг, регулятор regOfFamily u положителен и потому не равен нулю.

LaTeX

$$$\\text{If } \\text{IsMaxRank}(u) \\text{ then } regOfFamily u > 0.$$$

Lean4

theorem regOfFamily_of_isMaxRank {u : Fin (rank K) → (𝓞 K)ˣ} (hu : IsMaxRank u) :
    regOfFamily u = ZLattice.covolume (span ℤ (Set.range (basisOfIsMaxRank hu))) := by rw [regOfFamily, dif_pos hu]

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