Module

HasPrincipalDivisors_adjoin_of_transcendental.lean

Nyll.AlgebraicCurves.Divisors.HasPrincipalDivisors_adjoin_of_transcendental

2 declarations indexed from sourceView source ↗

Module documentation

Has Principal Divisors adjoin of transcendental

Imports2

Imported by1

Nyll.AlgebraicCurves.Divisors.All

theorem

hasPrincipalDivisors_adjoin

L33 ↗

AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_adjoin_of_transcendental.AlgebraicCurve.W2.hasPrincipalDivisors_adjoin

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_adjoin_of_transcendental
noncomputable section
open IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W2
variable (K : Type*) [Field K] [CharZero K] {LF : Type*} [Field LF] [Algebra K LF]

Lean source · statement

theorem hasPrincipalDivisors_adjoin (x : LF) (hx : Transcendental K x) (T : Finset LF)
    (hT : ∀ t ∈ T, IsIntegral (IntermediateField.adjoin K ({x} : Set LF)) t) :
    HasPrincipalDivisors K (IntermediateField.adjoin K (insert x (T : Set LF)))

theorem

hasPrincipalDivisors_adjoin_of_transcendental

L87 ↗

AlgebraicCurve.hasPrincipalDivisors_adjoin_of_transcendental

Source context 5 commands