IsIntegrallyClosed.exists_algebraMap_eq_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_exists_algebraMap_eq_of_forall_height_eq_oneLean source · statement
theorem _root_.IsIntegrallyClosed.exists_algebraMap_eq_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 →
∃ r s : R, s ∉ p ∧ x * algebraMap R K s = algebraMap R K r) :
∃ r : R, algebraMap R K r = x