minkowskiBound_lt_top — Mathlib

English

The Minkowski bound for a fractional ideal lattice is finite: minkowskiBound K I < ∞.

Русский

Границы Минковского для фракционного идеала конечны: minkowskiBound(K, I) < ∞.

LaTeX

$$$\text{minkowskiBound } K I < \top.$$$

Lean4

theorem minkowskiBound_lt_top : minkowskiBound K I < ⊤ := by
  classical
    -- FIXME: Make `finiteness` work here
    exact ENNReal.mul_lt_top (fundamentalDomain_isBounded _).measure_lt_top <| ENNReal.pow_lt_top ENNReal.ofNat_lt_top

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