SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 23:48:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

Merge pull request #65 from GTBarkley/monalisa

Browse source 
removed two imports
This commit is contained in:
ah1112 2023-06-14 16:38:05 -04:00 committed by GitHub
commit f5d4feccb1
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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' < ⊤}