valuation_eq_iff — Mathlib

English

Two elements x, y have the same valuation in A iff there exists a unit a in A with a*y = x.

Русский

Для элементов x, y верны A.valuation(x)=A.valuation(y) тогда и только тогда существует элемент-единица a в A такой, что a·y = x.

LaTeX

$$$A.valuation(x)=A.valuation(y) \iff \exists a:\, A^\times, (a:K)\cdot y = x$$$

Lean4

theorem valuation_eq_iff (x y : K) : A.valuation x = A.valuation y ↔ ∃ a : Aˣ, (a : K) * y = x :=
  Quotient.eq''

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