one_le_mult

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

English

As a corollary, mult w ≠ 0, and in particular the real cast is not zero.

Русский

Как следствие, mult w ≠ 0, и, в частности, образ в ℝ не равен нулю.

LaTeX

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

Lean4

theorem one_le_mult {w : InfinitePlace K} : (1 : ℝ) ≤ mult w :=
  by
  rw [← Nat.cast_one, Nat.cast_le]
  exact mult_pos

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

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

Разделы

Аффилиация

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