Theorems · Definition · commutative algebra

ValuativeRel.ValueGroupWithZero.mk

{R : Type u_1} →
  [inst : Semiring R] →
    [inst_1 : ValuativeRel R] → R → ↥(ValuativeRel.posSubmonoid R) → ValuativeRel.ValueGroupWithZero R

Construct an element of the value group-with-zero from an element r : R and y : posSubmonoid R. This should be thought of as v r / v y.

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

25 results in Mathlib

Foundations

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

Assumes

SemiringValuativeRel