Subalgebra.isIntegrallyClosed_adjoin_singleton_of_transcendental
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Subalgebra_isIntegrallyClosed_adjoin_singleton_of_transcendental
open PolynomialLean source · statement
theorem _root_.Subalgebra.isIntegrallyClosed_adjoin_singleton_of_transcendental
{L : Type*} [Field L] {F : Type*} [CommRing F] [IsDomain F] [Algebra L F]
(x : F) (hxL : Transcendental L x) :
IsIntegrallyClosed (Algebra.adjoin L ({x} : Set F))