Theorems · Theorem · commutative algebra

AddValuation.of_apply

∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (f : R → Γ₀)
  {h0 : f 0 = ⊤} {h1 : f 1 = 0} {hadd : ∀ (x y : R), min (f x) (f y) ≤ f (x + y)}
  {hmul : ∀ (x y : R), f (x * y) = f x + f y} {r : R}, (AddValuation.of f h0 h1 hadd hmul) r = f r

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingLinearOrderedAddCommMonoidWithTop