lift_valuation — Mathlib

English

For any function f with a compatibility condition hf, the lift of f at the valuation equals the base value with the trivial submonoid: lift f hf (valuation x) = f(x,1).

Русский

Для любой функции f с условием совместимости hf подъём функции, применённый к оцениванию, равен базовому значению с тривиальным подмоноидом: lift f hf (valuation x) = f(x,1).

LaTeX

$$$\mathrm{ValueGroupWithZero.lift} f\ hf (\mathrm{valuation}\, R\ x) = f(x,1)$$$

Lean4

@[simp]
theorem lift_valuation {α : Sort*} (f : R → posSubmonoid R → α)
    (hf : ∀ (x y : R) (t s : posSubmonoid R), x * t ≤ᵥ y * s → y * s ≤ᵥ x * t → f x s = f y t) (x : R) :
    ValueGroupWithZero.lift f hf (valuation R x) = f x 1 :=
  rfl

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