X_inv — Mathlib

English

For x,y, the valuation satisfies v(x+y) ≤ max(v(x), v(y)).

Русский

Для x, y валюация удовлетворяет v(x+y) ≤ max(v(x), v(y)).

LaTeX

$$$v(x+y) \le \max\{v(x), v(y)\}.$$$

Lean4

theorem X_inv : inftyValuation Fq (1 / RatFunc.X) = exp (-1) := by
  rw [one_div, ← zpow_neg_one, inftyValuation.X_zpow]
    -- Dropped attribute `@[simp]` due to issue described here:
    -- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60synthInstance.2EmaxHeartbeats.60.20error.20but.20only.20in.20.60simpNF.60

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