HenselianLocalRing.moduleFinite_localizationAtPrime_of_moduleFinite
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_moduleFinite_localizationAtPrime_of_moduleFinite
open IsLocalRing
open _root_.HenselianLocalRing
(exists_completeOrthogonalIdempotents_forall_isLocalRing_quotient_of_moduleFinite)Lean source · statement
theorem _root_.HenselianLocalRing.moduleFinite_localizationAtPrime_of_moduleFinite
{A : Type*} [CommRing A] [HenselianLocalRing A]
{B : Type*} [CommRing B] [Algebra A B] [Module.Finite A B]
(𝔫 : Ideal B) [𝔫.IsMaximal] :
Module.Finite A (Localization.AtPrime 𝔫)