pos_iff

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

English

For a fixed w ∈ InfinitePlace(K) and x ∈ K, 0 < w x if and only if x ≠ 0.

Русский

Для фиксированного w ∈ InfinitePlace(K) и элемента x ∈ K верно: 0 < w x тогда и только тогда, когда x ≠ 0.

LaTeX

$$$\\\\forall {w : \\\\mathrm{InfinitePlace}(K)}\\\\ {x : K}, \\\\ 0 < w x \\\\iff x \\neq 0.$$$

Lean4

theorem pos_iff {w : InfinitePlace K} {x : K} : 0 < w x ↔ x ≠ 0 :=
  AbsoluteValue.pos_iff w.1

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

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

Разделы

Аффилиация

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