Skip to content

Commit 0b2425f

Browse files
committed
chore(RingTheory/Valuation): move ValuativeRel to ValuativeRel.Basic (#28890)
in preparation for trivial rel and discrete rel files like in #27313 Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
1 parent 0162724 commit 0b2425f

File tree

6 files changed

+809
-800
lines changed

6 files changed

+809
-800
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5786,6 +5786,7 @@ import Mathlib.RingTheory.Valuation.ValExtension
57865786
import Mathlib.RingTheory.Valuation.ValuationRing
57875787
import Mathlib.RingTheory.Valuation.ValuationSubring
57885788
import Mathlib.RingTheory.Valuation.ValuativeRel
5789+
import Mathlib.RingTheory.Valuation.ValuativeRel.Basic
57895790
import Mathlib.RingTheory.WittVector.Basic
57905791
import Mathlib.RingTheory.WittVector.Compare
57915792
import Mathlib.RingTheory.WittVector.Complete

Mathlib/RingTheory/Valuation/RankOne.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ import Mathlib.Algebra.Order.Group.Units
77
import Mathlib.Algebra.Order.GroupWithZero.WithZero
88
import Mathlib.Analysis.SpecialFunctions.Pow.Real
99
import Mathlib.Data.Real.Embedding
10-
import Mathlib.RingTheory.Valuation.ValuativeRel
10+
import Mathlib.RingTheory.Valuation.ValuativeRel.Basic
1111

1212
/-!
1313
# Rank one valuations

0 commit comments

Comments
 (0)