map_add'

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#Valuation.map_add'

English

Then either v(x+y) ≤ v(x) or v(x+y) ≤ v(y).

Русский

Тогда либо v(x+y) ≤ v(x), либо v(x+y) ≤ v(y).

LaTeX

$$$ v(x+y) \le v(x) \quad \text{or} \quad v(x+y) \le v(y) $$$

Lean4

@[simp]
theorem map_add' : ∀ x y, v (x + y) ≤ v x ∨ v (x + y) ≤ v y :=
  by
  intro x y
  rw [← le_max_iff, ← ge_iff_le]
  apply v.map_add

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

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

Разделы

Аффилиация

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