valuation_le_iff

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#ValuationSubring.valuation_le_iff

English

For x,y in K, A.valuation x ≤ A.valuation y iff there exists a in A with a y = x.

Русский

Для x,y в K, A.valuation(x) ≤ A.valuation(y) тогда и только тогда существует a ∈ A, такой что a y = x.

LaTeX

$$$A.valuation(x) \le A.valuation(y) \iff \exists a:\, A, a\,y = x$$$

Lean4

theorem valuation_le_iff (x y : K) : A.valuation x ≤ A.valuation y ↔ ∃ a : A, (a : K) * y = x :=
  Iff.rfl

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

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

Разделы

Аффилиация

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