AlgebraicCurve.exists_divisor_eq_max_ord_sub_algebraMap
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_divisor_eq_max_ord_sub_algebraMap
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.exists_divisor_eq_max_ord_sub_algebraMap
{K F : Type*} [Field K] [Field F] [Algebra K F] [HasPrincipalDivisors K F]
(x : F) (hx : Transcendental K x) (a : K) :
∃ D : Divisor K F, ∀ v : Place K F, D v = max 0 (v.ord (x - algebraMap K F a))