Skip to content

Commit c9e6ed7

Browse files
feat: port RingTheory.Multiplicity (#2962)
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
1 parent 45b747d commit c9e6ed7

File tree

2 files changed

+670
-0
lines changed

2 files changed

+670
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1271,6 +1271,7 @@ import Mathlib.RingTheory.Ideal.Prod
12711271
import Mathlib.RingTheory.Ideal.Quotient
12721272
import Mathlib.RingTheory.Localization.Basic
12731273
import Mathlib.RingTheory.Localization.Integer
1274+
import Mathlib.RingTheory.Multiplicity
12741275
import Mathlib.RingTheory.MvPolynomial.Tower
12751276
import Mathlib.RingTheory.Nilpotent
12761277
import Mathlib.RingTheory.NonZeroDivisors

0 commit comments

Comments
 (0)