emin

Mathlib.Data.FP.Basic

URI: https://scilib.ai/kg/mathlib#FP.emin

English

The minimal exponent is defined by emin = 1 − C.emax.

Русский

Минимальная экспонента равна emin = 1 − C.emax.

LaTeX

$$$\\mathrm{emin} = 1 - C.emax$$$

Lean4

@[nolint docBlame]
def emin : ℤ :=
  1 - C.emax

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

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

Разделы

Аффилиация

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