map_div

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#AddValuation.map_div

English

For a valuation v on a field K, v(x/y) = v(x) − v(y).

Русский

Для оценки v на поле K: v(x/y) = v(x) − v(y).

LaTeX

$$$$ v\\left( \\frac{x}{y} \\right) = v(x) - v(y). $$$$

Lean4

@[simp]
theorem map_div (v : AddValuation K Γ₀) {x y : K} : v (x / y) = v x - v y :=
  map_div₀ (toValuation v) x y

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

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

Разделы

Аффилиация

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