AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_integralClosure_le_of_isUnit_discr_of_span_eq_top.IntegralClosureLeOfIsUnitDiscr.isLocalization_of_span_eq_top
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_integralClosure_le_of_isUnit_discr_of_span_eq_top
open Matrix
open scoped nonZeroDivisors
namespace IntegralClosureLeOfIsUnitDiscr
open _root_.Algebra
variable {R : Type*} [CommRing R] [IsDomain R]
{K : Type*} [Field K] [Algebra R K] [IsFractionRing R K]
{A : Type*} [CommRing A] [Algebra K A] [Algebra R A] [IsScalarTower R K A]Lean source · statement
theorem isLocalization_of_span_eq_top (S : Subalgebra R A)
(hS : Submodule.span K ((S : Subalgebra R A) : Set A) = ⊤) :
IsLocalization (Algebra.algebraMapSubmonoid S R⁰) A