Theorems · Definition · commutative algebra

AddValuation.of

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

An alternate constructor of AddValuation, that doesn't reference Multiplicative Γ₀ᵒᵈ

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingLinearOrderedAddCommMonoidWithTop