SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-10-16 19:43:55 -05:00
Code Issues Projects Releases Packages Wiki Activity

removed two imports

Browse source
This commit is contained in:
Andre 2023-06-14 16:37:08 -04:00
parent cf7f08df3e
commit a62a8bfe4d
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
CommAlg/monalisa.lean
View file

@ -4,8 +4,6 @@ import Mathlib.Algebra.Module.GradedModule
import Mathlib.RingTheory.Ideal.AssociatedPrime import Mathlib.RingTheory.Ideal.AssociatedPrime
import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Artinian
import Mathlib.Order.Height import Mathlib.Order.Height
import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Mathlib.RingTheory.FiniteType
noncomputable def length ( A : Type _) (M : Type _) noncomputable def length ( A : Type _) (M : Type _)
[CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤} [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤}