SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2025-04-11 15:26:03 -05:00
Code Issues Projects Releases Packages Wiki Activity

removed imports

Browse source
This commit is contained in:
Andre 2023-06-14 15:07:21 -04:00
parent 01ac7a2777
commit a1888c51e6
1 changed files with 0 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
CommAlg/monalisa.lean
View file

@ -1,31 +1,9 @@
import Mathlib.Order.KrullDimension import Mathlib.Order.KrullDimension
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
import Mathlib.RingTheory.Ideal.Operations
import Mathlib.LinearAlgebra.Finsupp
import Mathlib.RingTheory.GradedAlgebra.Basic
import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
import Mathlib.Algebra.Module.GradedModule import Mathlib.Algebra.Module.GradedModule
import Mathlib.RingTheory.Ideal.AssociatedPrime import Mathlib.RingTheory.Ideal.AssociatedPrime
import Mathlib.RingTheory.Noetherian
import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Artinian
import Mathlib.RingTheory.FiniteType
import Mathlib.Order.Height import Mathlib.Order.Height
import Mathlib.RingTheory.PrincipalIdealDomain
import Mathlib.RingTheory.DedekindDomain.Basic
import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.RingTheory.Localization.AtPrime
import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Mathlib.Algebra.DirectSum.Ring
import Mathlib.RingTheory.Ideal.LocalRing
--import Mathlib
import Mathlib.Algebra.MonoidAlgebra.Basic
import Mathlib.Data.Finset.Sort
import Mathlib.Order.JordanHolder
import Mathlib.RingTheory.Ideal.Basic
import Mathlib.RingTheory.Finiteness
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' < ⊤}