mult_ne_zero

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

English

For any infinite place w, mult(w) ≠ 0.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mult_ne_zero {w : InfinitePlace K} : mult w ≠ 0 :=
  ne_of_gt mult_pos

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

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

Разделы

Аффилиация

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