AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_isLocalRing_of_isDomain_of_moduleFinite.S17Hens.isArtinianRing_quotient_map_maximalIdeal
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_isLocalRing_of_isDomain_of_moduleFinite
universe u v
namespace S17HensLean source · statement
theorem isArtinianRing_quotient_map_maximalIdeal
{R : Type u} [CommRing R] [IsLocalRing R]
{S : Type v} [CommRing S] [Algebra R S] [Module.Finite R S] :
IsArtinianRing (S ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S))