Theorems · Inductive type · commutative algebra

Valued

(R : Type u) → [Ring R] → (Γ₀ : outParam (Type v)) → [LinearOrderedCommGroupWithZero Γ₀] → Type (max u v)

A valued ring is a ring that comes equipped with a distinguished valuation. The class Valued is designed for the situation that there is a canonical valuation on the ring. TODO: show that there always exists an equivalent valuation taking values in a type belonging to the same universe as the ring. See Note [forgetful inheritance] for why we extend UniformSpace, IsUniformAddGroup.

Defined in

Mathlib.Topology.Algebra.Valued.ValuationTopology

Cited by

70 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

RingLinearOrderedCommGroupWithZero