Theorems · Theorem · commutative algebra

ValuativeRel.ValueGroupWithZero.lift_mul

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

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringValuativeRelMul