Theorems · Theorem · commutative algebra

ValuativeRel.ValueGroupWithZero.lift.congr_simp

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

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringValuativeRel