covolume_pos

Mathlib.Algebra.Module.ZLattice.Covolume

URI: https://scilib.ai/kg/mathlib#ZLattice.covolume_pos

English

The covolume of L is strictly positive: 0 < covolume(L, μ).

Русский

Коволюм L строго положителен: 0 < covolume(L, μ).

LaTeX

$$$0 < \\operatorname{covolume}(L,\\mu)$$$

Lean4

theorem covolume_pos : 0 < covolume L μ :=
  lt_of_le_of_ne ENNReal.toReal_nonneg (covolume_ne_zero L μ).symm

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

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

Разделы

Аффилиация

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