regOfFamily_pos

Mathlib.NumberTheory.NumberField.Units.Regulator

URI: https://scilib.ai/kg/mathlib#NumberField.Units.regOfFamily_pos

← MathLib Explorer

English

regOfFamily u is nonzero if and only if u has maximal rank.

Русский

regOfFamily u не равен нулю тогда, когда у имеет максимальный ранг и наоборот.

LaTeX

$$$regOfFamily u \\neq 0 \\iff IsMaxRank u$$$

Lean4

theorem regOfFamily_pos {u : Fin (rank K) → (𝓞 K)ˣ} (hu : IsMaxRank u) : 0 < regOfFamily u := by
  classical
  rw [regOfFamily_of_isMaxRank hu]
  exact ZLattice.covolume_pos _ volume

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru