AlgebraicCurve.hasPrincipalDivisors_of_transcendental_of_isSeparable
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental_of_isSeparable
open AlgebraicCurve IntermediateField
noncomputable sectionLean source · statement
theorem _root_.AlgebraicCurve.hasPrincipalDivisors_of_transcendental_of_isSeparable {K F :
Type*} [Field K] [Field F] [Algebra K F]
{x : F} (htr : Transcendental K x)
(hfd : FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
(hsep : Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F) :
HasPrincipalDivisors K F