Skip to content

Commit a9138cd

Browse files
feat: port RingTheory.Valuation.Basic (#2846)
Co-authored-by: Matthew Ballard <matt@mrb.email>
1 parent 27f3e68 commit a9138cd

File tree

2 files changed

+928
-0
lines changed

2 files changed

+928
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1274,6 +1274,7 @@ import Mathlib.RingTheory.Subring.Basic
12741274
import Mathlib.RingTheory.Subring.Pointwise
12751275
import Mathlib.RingTheory.Subsemiring.Basic
12761276
import Mathlib.RingTheory.Subsemiring.Pointwise
1277+
import Mathlib.RingTheory.Valuation.Basic
12771278
import Mathlib.SetTheory.Cardinal.Basic
12781279
import Mathlib.SetTheory.Cardinal.Cofinality
12791280
import Mathlib.SetTheory.Cardinal.Continuum

0 commit comments

Comments
 (0)