IsIntegrallyClosed.mem_range_algebraMap_of_forall_height_eq_one
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_mem_range_algebraMap_of_forall_height_eq_oneLean source · statement
theorem _root_.IsIntegrallyClosed.mem_range_algebraMap_of_forall_height_eq_one
{R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R]
{K : Type*} [Field K] [Algebra R K] [IsFractionRing R K]
(x : K)
(hx : ∀ P : Ideal R, P.IsPrime → P.height = 1 →
∃ a s : R, s ∉ P ∧ x * algebraMap R K s = algebraMap R K a) :
x ∈ Set.range (algebraMap R K)