mult_pos

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.InfinitePlace.mult_pos

English

For every infinite place w of K, mult(w) > 0.

Русский

Для каждого бесконечного места w поля K выполняется, что mult(w) > 0.

LaTeX

$$$\forall w : \mathrm{InfinitePlace} K, \operatorname{mult}(w) > 0$$$

Lean4

theorem mult_pos {w : InfinitePlace K} : 0 < mult w := by
  rw [mult]
  split_ifs <;> norm_num

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

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

Разделы

Аффилиация

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