Def ValuativeRel.trivialRel

Modification history

2026-06-03 06:54

Mathlib/RingTheory/Valuation/ValuativeRel/Trivial.lean

feat(Valuation/ValuativeRel): generalize `ValuativeRel` to non-commutative rings (#36777) …

Modified ValuativeRel.trivialRel View on Github →

2025-09-29 16:33

Mathlib/RingTheory/Valuation/ValuativeRel/Trivial.lean

feat(RingTheory/ValuativeRel/Trivial): the trivial valuative relation (#27313) …

Added ValuativeRel.trivialRel View on Github →