Theorems · Definition · commutative algebra

ValuativeRel.ValueGroupWithZero.lift

{R : Type u_1} →
  [inst : Semiring R] →
    [inst_1 : ValuativeRel R] →
      {α : Sort u_2} →
        (f : R → ↥(ValuativeRel.posSubmonoid R) → α) →
          (∀ (x y : R) (t s : ↥(ValuativeRel.posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) →
            ValuativeRel.ValueGroupWithZero R → α

Lifts a function R → posSubmonoid R → α to the value group-with-zero of R.

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

6 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringValuativeRel