noncomputable def AbsoluteHeight.absoluteHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (P : Projectivization K (ι → K)) : ℝ

theorem AbsoluteHeight.absoluteHeight_mk {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] {x : ι → K} (hx : x ≠ 0) : absoluteHeight (Projectivization.mk K x hx) = Height.mulHeight x

noncomputable def AbsoluteHeight.logHeight {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (P : Projectivization K (ι → K)) : ℝ

theorem AbsoluteHeight.logHeight_eq {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (P : Projectivization K (ι → K)) : logHeight P = P.logHeight

theorem weil_height_ge_one {K : Type u_1} [Field K] [NumberField K] {n : ℕ} (x : Fin (n + 1) → K) : 1 ≤ Height.mulHeight x

theorem height_morphism_upper_bound {K : Type u_1} [Field K] [NumberField K] {n m d : ℕ} {φ : Fin (m + 1) → MvPolynomial (Fin (n + 1)) K} (hφ : ∀ (i : Fin (m + 1)), (φ i).IsHomogeneous d) : ∃ (c : ℝ), ∀ (x : Fin (n + 1) → K), (Height.logHeight fun (j : Fin (m + 1)) => (MvPolynomial.eval x) (φ j)) ≤ ↑d * Height.logHeight x + c

theorem height_automorphism_bound {K : Type u_1} [Field K] [NumberField K] {n : ℕ} {φ ψ : Fin (n + 1) → MvPolynomial (Fin (n + 1)) K} (hφ : ∀ (i : Fin (n + 1)), (φ i).IsHomogeneous 1) (hψ : ∀ (i : Fin (n + 1)), (ψ i).IsHomogeneous 1) (hinv : ∀ (x : Fin (n + 1) → K) (i : Fin (n + 1)), (MvPolynomial.eval fun (j : Fin (n + 1)) => (MvPolynomial.eval x) (φ j)) (ψ i) = x i) : ∃ (c : ℝ), ∀ (x : Fin (n + 1) → K), |(Height.logHeight fun (j : Fin (n + 1)) => (MvPolynomial.eval x) (φ j)) - Height.logHeight x| ≤ c

theorem NumberField.FinitePlace.isFinitePlace_comp_galois {K : Type u_1} [Field K] [NumberField K] (σ : Gal(K/ℚ)) (v : FinitePlace K) : ∃ (w : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), place (embedding w) = (↑v).comp ⋯

noncomputable def galoisEquivFinitePlace {K : Type u_1} [Field K] [NumberField K] (σ : Gal(K/ℚ)) : NumberField.FinitePlace K ≃ NumberField.FinitePlace K

theorem galoisEquivFinitePlace_apply {K : Type u_1} [Field K] [NumberField K] (σ : Gal(K/ℚ)) (v : NumberField.FinitePlace K) (y : K) : ((galoisEquivFinitePlace σ) v) y = v (σ.symm y)

theorem prod_infinitePlace_galois_eq {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (σ : Gal(K/ℚ)) (x : ι → K) : ∏ v : NumberField.InfinitePlace K, (⨆ (i : ι), v (σ (x i))) ^ v.mult = ∏ v : NumberField.InfinitePlace K, (⨆ (i : ι), v (x i)) ^ v.mult

theorem finprod_finitePlace_galois_eq {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (σ : Gal(K/ℚ)) (x : ι → K) : ∏ᶠ (v : NumberField.FinitePlace K), ⨆ (i : ι), v (σ (x i)) = ∏ᶠ (v : NumberField.FinitePlace K), ⨆ (i : ι), v (x i)

theorem mulHeight_galois_invariant {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (σ : Gal(K/ℚ)) (x : ι → K) : Height.mulHeight (⇑σ ∘ x) = Height.mulHeight x

theorem logHeight_galois_invariant {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (σ : Gal(K/ℚ)) (x : ι → K) : Height.logHeight (⇑σ ∘ x) = Height.logHeight x

structure EllipticCurve.WeakMordellWeil.TwoIsogenyData (W : WeierstrassCurve ℚ) [W.IsElliptic] : Type 1

• E'Points : Type
• instAddCommGroup : AddCommGroup self.E'Points
• phi : W.toAffine.Point →+ self.E'Points
• phi_hat : self.E'Points →+ W.toAffine.Point
• comp_eq : self.phi_hat.comp self.phi = zsmulAddGroupHom 2
• descentTarget : Type
• instDescentTargetGroup : AddCommGroup self.descentTarget
• descentMap : self.E'Points →+ self.descentTarget
• descentMap_range_finite : Finite ↥self.descentMap.range
• descentMap_ker_eq : self.descentMap.ker = self.phi.range
• descentTarget' : Type
• instDescentTarget'Group : AddCommGroup self.descentTarget'
• descentMap' : W.toAffine.Point →+ self.descentTarget'
• descentMap'_range_finite : Finite ↥self.descentMap'.range
• descentMap'_ker_eq : self.descentMap'.ker = self.phi_hat.range
• phi_hat_ker_le_phi_range : self.phi_hat.ker ≤ self.phi.range

def EllipticCurve.WeakMordellWeil.IsNonzeroSquare (q : ℚ) : Prop

theorem EllipticCurve.WeakMordellWeil.lemma_25_3_phi {W : WeierstrassCurve ℚ} [W.IsElliptic] (data : TwoIsogenyData W) : data.descentMap.ker = data.phi.range

theorem EllipticCurve.WeakMordellWeil.lemma_25_3_phi_hat {W : WeierstrassCurve ℚ} [W.IsElliptic] (data : TwoIsogenyData W) : data.descentMap'.ker = data.phi_hat.range

def EllipticCurve.WeakMordellWeil.E'Curve (a b : ℚ) : WeierstrassCurve ℚ

noncomputable def EllipticCurve.WeakMordellWeil.descentMapRaw (a b : ℚ) (hdisc : a ^ 2 - 4 * b ≠ 0) : (E'Curve a b).toAffine.Point → Additive (ℚˣ ⧸ Subgroup.square ℚˣ)

theorem EllipticCurve.WeakMordellWeil.square_class_self_add (g : ℚˣ ⧸ Subgroup.square ℚˣ) : Additive.ofMul g + Additive.ofMul g = 0

theorem EllipticCurve.WeakMordellWeil.square_class_mk_mul (x y : ℚ) (hx : x ≠ 0) (hy : y ≠ 0) : (QuotientGroup.mk' (Subgroup.square ℚˣ)) (Units.mk0 (x * y) ⋯) = (QuotientGroup.mk' (Subgroup.square ℚˣ)) (Units.mk0 x hx) * (QuotientGroup.mk' (Subgroup.square ℚˣ)) (Units.mk0 y hy)

theorem EllipticCurve.WeakMordellWeil.square_class_mul_eq_div (x y : ℚ) (hx : x ≠ 0) (hy : y ≠ 0) : (QuotientGroup.mk' (Subgroup.square ℚˣ)) (Units.mk0 (x * y) ⋯) = (QuotientGroup.mk' (Subgroup.square ℚˣ)) (Units.mk0 (x / y) ⋯)

theorem EllipticCurve.WeakMordellWeil.descentMapRaw_add_nonInverse (a b : ℚ) (hE' : (E'Curve a b).IsElliptic) (hdisc : a ^ 2 - 4 * b ≠ 0) (x₁ x₂ y₁ y₂ : ℚ) (h₁ : (E'Curve a b).toAffine.Nonsingular x₁ y₁) (h₂ : (E'Curve a b).toAffine.Nonsingular x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = (E'Curve a b).toAffine.negY x₂ y₂)) : descentMapRaw a b hdisc (WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ + WeierstrassCurve.Affine.Point.some x₂ y₂ h₂) = descentMapRaw a b hdisc (WeierstrassCurve.Affine.Point.some x₁ y₁ h₁) + descentMapRaw a b hdisc (WeierstrassCurve.Affine.Point.some x₂ y₂ h₂)

theorem EllipticCurve.WeakMordellWeil.descentMapRaw_add (a b : ℚ) (hE' : (E'Curve a b).IsElliptic) (hdisc : a ^ 2 - 4 * b ≠ 0) (P Q : (E'Curve a b).toAffine.Point) : descentMapRaw a b hdisc (P + Q) = descentMapRaw a b hdisc P + descentMapRaw a b hdisc Q

noncomputable def EllipticCurve.WeakMordellWeil.descentMapHom (a b : ℚ) (hE' : (E'Curve a b).IsElliptic) (hdisc : a ^ 2 - 4 * b ≠ 0) : (E'Curve a b).toAffine.Point →+ Additive (ℚˣ ⧸ Subgroup.square ℚˣ)

theorem EllipticCurve.WeakMordellWeil.lemma_25_4_concrete (a b : ℚ) (hE' : (E'Curve a b).IsElliptic) (hdisc : a ^ 2 - 4 * b ≠ 0) : ∃ (π : (E'Curve a b).toAffine.Point →+ Additive (ℚˣ ⧸ Subgroup.square ℚˣ)), (∀ (x y : ℚ) (hxy : (E'Curve a b).toAffine.Nonsingular x y) (hx : x ≠ 0), π (WeierstrassCurve.Affine.Point.some x y hxy) = Additive.ofMul ((QuotientGroup.mk' (Subgroup.square ℚˣ)) (Units.mk0 x hx))) ∧ ∀ (hns : (E'Curve a b).toAffine.Nonsingular 0 0), π (WeierstrassCurve.Affine.Point.some 0 0 hns) = Additive.ofMul ((QuotientGroup.mk' (Subgroup.square ℚˣ)) (Units.mk0 (a ^ 2 - 4 * b) hdisc))

theorem EllipticCurve.WeakMordellWeil.sq_class_of_rat_unit (u : ℚˣ) : (QuotientGroup.mk' (Subgroup.square ℚˣ)) u = (QuotientGroup.mk' (Subgroup.square ℚˣ)) (Units.mk0 ↑((↑u).num * ↑(↑u).den) ⋯)

theorem EllipticCurve.WeakMordellWeil.int_sq_mul_squarefree (n : ℤ) (hn : n ≠ 0) : ∃ (r : ℤ) (s : ℤ), n = r * s ^ 2 ∧ Squarefree r ∧ r ≠ 0 ∧ s ≠ 0

theorem EllipticCurve.WeakMordellWeil.sq_class_of_sq_factor (n r s : ℤ) (hn : n ≠ 0) (hr : r ≠ 0) (hs : s ≠ 0) (heq : n = r * s ^ 2) : (QuotientGroup.mk' (Subgroup.square ℚˣ)) (Units.mk0 ↑n ⋯) = (QuotientGroup.mk' (Subgroup.square ℚˣ)) (Units.mk0 ↑r ⋯)

theorem EllipticCurve.WeakMordellWeil.squarefree_part_dvd_target (A B : ℚ) (hB : B ≠ 0) (u : ℚˣ) (Y : ℚ) (hY : Y ^ 2 = ↑u * (↑u ^ 2 + A * ↑u + B)) (hN : ↑A.den * B.num * ↑B.den ≠ 0) (r s : ℤ) (hr_sf : Squarefree r) (hr_ne : r ≠ 0) (hs_ne : s ≠ 0) (heq : (↑u).num * ↑(↑u).den = r * s ^ 2) : r ∣ ↑A.den * B.num * ↑B.den

theorem EllipticCurve.WeakMordellWeil.sq_class_curve_divides_B (A B : ℚ) (hB : B ≠ 0) (u : ℚˣ) (Y : ℚ) (hY : Y ^ 2 = ↑u * (↑u ^ 2 + A * ↑u + B)) (hN : ↑A.den * B.num * ↑B.den ≠ 0) : ∃ (d : ℤ) (hd : d ∣ ↑A.den * B.num * ↑B.den), (QuotientGroup.mk' (Subgroup.square ℚˣ)) u = (QuotientGroup.mk' (Subgroup.square ℚˣ)) (Units.mk0 ↑d ⋯)

theorem EllipticCurve.WeakMordellWeil.corollary_25_6 (W : WeierstrassCurve ℚ) [W.IsElliptic] (data : TwoIsogenyData W) : data.phi.range.FiniteIndex ∧ data.phi_hat.range.FiniteIndex

theorem EllipticCurve.WeakMordellWeil.corollary_25_7_index (W : WeierstrassCurve ℚ) [W.IsElliptic] (data : TwoIsogenyData W) : (zsmulAddGroupHom 2).range.index = data.phi.range.index * data.phi_hat.range.index

theorem EllipticCurve.WeakMordellWeil.corollary_25_7 (W : WeierstrassCurve ℚ) [W.IsElliptic] (data : TwoIsogenyData W) : (zsmulAddGroupHom 2).range.FiniteIndex

theorem EllipticCurve.WeakMordellWeil.corollary_25_7' (W : WeierstrassCurve ℚ) [W.IsElliptic] (data : TwoIsogenyData W) : Finite (W.toAffine.Point ⧸ (zsmulAddGroupHom 2).range)

noncomputable def CanonicalHeight.canonicalHeightSeq {E : Type u_1} [AddCommGroup E] (h : E → ℝ) (P : E) (n : ℕ) : ℝ

noncomputable def CanonicalHeight.canonicalHeight {E : Type u_1} [AddCommGroup E] (h : E → ℝ) (P : E) : ℝ

theorem CanonicalHeight.canonicalHeightSeq_double {E : Type u_1} [AddCommGroup E] (h : E → ℝ) (P : E) (n : ℕ) : canonicalHeightSeq h (2 • P) n = 4 * canonicalHeightSeq h P (n + 1)

theorem CanonicalHeight.canonicalHeight_double {E : Type u_1} [AddCommGroup E] (h : E → ℝ) (P : E) (hconv : Filter.Tendsto (canonicalHeightSeq h P) Filter.atTop (nhds (canonicalHeight h P))) : canonicalHeight h (2 • P) = 4 * canonicalHeight h P

structure IsWeilHeightOnCurve {K : Type u_1} [Field K] (W : WeierstrassCurve K) (h : W.toAffine.Point → ℝ) : Prop

• doubling_bound : ∃ (C : ℝ), ∀ (P : W.toAffine.Point), |h (2 • P) - 4 * h P| ≤ C
• height_nonneg_zero : 0 ≤ h 0
• northcott (B : ℝ) : {P : W.toAffine.Point | h P ≤ B}.Finite

noncomputable def EllipticCurve.NeronTateHeight {K : Type u_1} [Field K] (W : WeierstrassCurve K) (h : W.toAffine.Point → ℝ) (_hWeil : IsWeilHeightOnCurve W h) (P : W.toAffine.Point) : ℝ

theorem EllipticCurve.neronTateHeight_parallelogram_law {K : Type u_1} [Field K] [NumberField K] (W : WeierstrassCurve K) [W.IsElliptic] [NumberField K] [W.IsElliptic] (h : W.toAffine.Point → ℝ) (hWeil : IsWeilHeightOnCurve W h) (P Q : W.toAffine.Point) : NeronTateHeight W h hWeil (P + Q) + NeronTateHeight W h hWeil (P - Q) = 2 * NeronTateHeight W h hWeil P + 2 * NeronTateHeight W h hWeil Q

noncomputable def TateTheorem.tateSeq {S : Type u_1} (φ : S → S) (h : S → ℝ) (r : ℝ) (x : S) (n : ℕ) : ℝ

@[simp]

theorem TateTheorem.tateSeq_zero {S : Type u_1} (φ : S → S) (h : S → ℝ) (r : ℝ) (x : S) : tateSeq φ h r x 0 = h x

theorem TateTheorem.tateSeq_dist {S : Type u_1} (φ : S → S) (h : S → ℝ) (r : ℝ) (hr : 1 < r) (C : ℝ) (hbound : ∀ (x : S), |h (φ x) - r * h x| ≤ C) (x : S) (n : ℕ) : dist (tateSeq φ h r x n) (tateSeq φ h r x (n + 1)) ≤ C / r ^ (n + 1)

theorem TateTheorem.summable_tate_bound {r : ℝ} (hr : 1 < r) (C : ℝ) : Summable fun (n : ℕ) => C / r ^ (n + 1)

theorem TateTheorem.tsum_tate_bound (r : ℝ) (hr : 1 < r) (C : ℝ) : ∑' (n : ℕ), C / r ^ (n + 1) = C / (r - 1)

theorem TateTheorem.tateSeq_cauchySeq {S : Type u_1} (φ : S → S) (h : S → ℝ) (r : ℝ) (hr : 1 < r) (C : ℝ) (hbound : ∀ (x : S), |h (φ x) - r * h x| ≤ C) (x : S) : CauchySeq (tateSeq φ h r x)

theorem TateTheorem.tateSeq_tendsto {S : Type u_1} (φ : S → S) (h : S → ℝ) (r : ℝ) (hr : 1 < r) (C : ℝ) (hbound : ∀ (x : S), |h (φ x) - r * h x| ≤ C) (x : S) : Filter.Tendsto (tateSeq φ h r x) Filter.atTop (nhds (Filter.atTop.limUnder (tateSeq φ h r x)))

theorem TateTheorem.tateSeq_comp {S : Type u_1} (φ : S → S) (h : S → ℝ) (r : ℝ) (hr : 1 < r) (x : S) (n : ℕ) : tateSeq φ h r (φ x) n = r * tateSeq φ h r x (n + 1)

theorem TateTheorem.tate_bound {S : Type u_1} (φ : S → S) (h : S → ℝ) (r : ℝ) (hr : 1 < r) (C : ℝ) (hbound : ∀ (x : S), |h (φ x) - r * h x| ≤ C) (x : S) : |Filter.atTop.limUnder (tateSeq φ h r x) - h x| ≤ C / (r - 1)

theorem TateTheorem.tate_comp_eq {S : Type u_1} (φ : S → S) (h : S → ℝ) (r : ℝ) (hr : 1 < r) (C : ℝ) (hbound : ∀ (x : S), |h (φ x) - r * h x| ≤ C) (x : S) : Filter.atTop.limUnder (tateSeq φ h r (φ x)) = r * Filter.atTop.limUnder (tateSeq φ h r x)

theorem TateTheorem.iterate_eq_of_comp {S : Type u_1} (φ : S → S) (f : S → ℝ) (r : ℝ) (hf_comp : ∀ (x : S), f (φ x) = r * f x) (x : S) (n : ℕ) : f (φ^[n] x) = r ^ n * f x

theorem TateTheorem.tateSeq_const_of_comp {S : Type u_1} (φ : S → S) (f : S → ℝ) (r : ℝ) (hr : 1 < r) (hf_comp : ∀ (x : S), f (φ x) = r * f x) (x : S) (n : ℕ) : tateSeq φ f r x n = f x

theorem TateTheorem.tendsto_div_pow_zero (r : ℝ) (hr : 1 < r) (D : ℝ) : Filter.Tendsto (fun (n : ℕ) => D / r ^ n) Filter.atTop (nhds 0)

theorem TateTheorem.tateSeq_diff_bound {S : Type u_1} (φ : S → S) (f h : S → ℝ) (r : ℝ) (hr : 1 < r) (D : ℝ) (hD : ∀ (x : S), |f x - h x| ≤ D) (x : S) (n : ℕ) : ‖tateSeq φ f r x n - tateSeq φ h r x n‖ ≤ D / r ^ n

theorem TateTheorem.tate_unique {S : Type u_1} (φ : S → S) (h : S → ℝ) (r : ℝ) (hr : 1 < r) (C : ℝ) (hbound : ∀ (x : S), |h (φ x) - r * h x| ≤ C) (f : S → ℝ) (D : ℝ) (hD : ∀ (x : S), |f x - h x| ≤ D) (hf_comp : ∀ (x : S), f (φ x) = r * f x) (x : S) : f x = Filter.atTop.limUnder (tateSeq φ h r x)

theorem TateTheorem.tate_theorem {S : Type u_1} (φ : S → S) (h : S → ℝ) (r : ℝ) (hr : 1 < r) (C : ℝ) (hbound : ∀ (x : S), |h (φ x) - r * h x| ≤ C) : (∀ (x : S), ∃ (L : ℝ), Filter.Tendsto (tateSeq φ h r x) Filter.atTop (nhds L)) ∧ (∀ (x : S), |Filter.atTop.limUnder (tateSeq φ h r x) - h x| ≤ C / (r - 1)) ∧ (∀ (x : S), Filter.atTop.limUnder (tateSeq φ h r (φ x)) = r * Filter.atTop.limUnder (tateSeq φ h r x)) ∧ ∀ (f : S → ℝ) (D : ℝ), (∀ (x : S), |f x - h x| ≤ D) → (∀ (x : S), f (φ x) = r * f x) → ∀ (x : S), f x = Filter.atTop.limUnder (tateSeq φ h r x)

theorem Northcott.finite_roots_of_bounded_mahler_degree (d : ℕ) (B : NNReal) : {α : ℂ | ∃ (p : Polynomial ℤ), p ≠ 0 ∧ p.natDegree ≤ d ∧ (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure ≤ ↑B ∧ (Polynomial.map (Int.castRingHom ℂ) p).IsRoot α}.Finite

theorem Northcott.mahlerMeasure_intNorm_minpoly_le_height_ax (K : Type u_1) [Field K] [NumberField K] (x : K) : (Polynomial.map (Int.castRingHom ℂ) (IsLocalization.integerNormalization (nonZeroDivisors ℤ) (minpoly ℚ x))).mahlerMeasure ≤ Height.mulHeight₁ x ^ Module.finrank ℚ K

theorem Northcott.mahlerMeasure_intNorm_minpoly_le_height (K : Type u_1) [Field K] [NumberField K] (x : K) : (Polynomial.map (Int.castRingHom ℂ) (IsLocalization.integerNormalization (nonZeroDivisors ℤ) (minpoly ℚ x))).mahlerMeasure ≤ Height.mulHeight₁ x ^ Module.finrank ℚ K

theorem Northcott.exists_intPoly_of_mulHeight₁_le (K : Type u_1) [Field K] [NumberField K] (σ : K →+* ℂ) (x : K) (B : NNReal) (hxB : Height.mulHeight₁ x ≤ ↑B) : ∃ (p : Polynomial ℤ), p ≠ 0 ∧ p.natDegree ≤ Module.finrank ℚ K ∧ (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure ≤ ↑(B ^ Module.finrank ℚ K) ∧ (Polynomial.map (Int.castRingHom ℂ) p).IsRoot (σ x)

theorem Northcott.finite_of_mulHeight₁_le (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : {x : K | Height.mulHeight₁ x ≤ B}.Finite

theorem Northcott.mulHeight₁_le_mulHeight_of_one_eq {K : Type u_1} [Field K] [NumberField K] {n : ℕ} (x : Fin (n + 1) → K) (_hx : x ≠ 0) (i₀ : Fin (n + 1)) (hi₀ : x i₀ = 1) (j : Fin (n + 1)) : Height.mulHeight₁ (x j) ≤ Height.mulHeight x

noncomputable def Northcott.mapCoords {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] (σ : K →+* L) (n : ℕ) : (Fin (n + 1) → K) →ₛₗ[σ] Fin (n + 1) → L

theorem Northcott.mapCoords_injective {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] {σ : K →+* L} (hσ : Function.Injective ⇑σ) (n : ℕ) : Function.Injective ⇑(mapCoords σ n)

theorem Northcott.northcott_theorem_25_18 (n d : ℕ) (B : ℝ) : {P : Projectivization ℂ (Fin (n + 1) → ℂ) | ∃ (K : Type) (x : Field K) (x_1 : NumberField K) (σ : K →+* ℂ), Module.finrank ℚ K ≤ d ∧ ∃ (Q : Projectivization K (Fin (n + 1) → K)), Q.mulHeight ≤ B ∧ P = Projectivization.map (mapCoords σ n) ⋯ Q}.Finite

theorem addGroup_fg_of_height_descent {G : Type u_1} [AddCommGroup G] (ĥ : G → ℝ) (hĥ_nonneg : ∀ (P : G), 0 ≤ ĥ P) (hĥ_double : ∀ (P : G), ĥ (2 • P) = 4 * ĥ P) (hĥ_par : ∀ (P Q : G), ĥ (P + Q) + ĥ (P - Q) = 2 * ĥ P + 2 * ĥ Q) (hquot : Finite (G ⧸ (zsmulAddGroupHom 2).range)) (hNorthcott : ∀ (B : ℝ), {P : G | ĥ P ≤ B}.Finite) : AddGroup.FG G

def IsProjectiveMorphism {K : Type u_1} [CommRing K] {n m : ℕ} (d : ℕ) (φ : Fin (m + 1) → MvPolynomial (Fin (n + 1)) K) : Prop

theorem projective_nullstellensatz_cofactors {K : Type u_1} [Field K] {n m d : ℕ} {φ : Fin (m + 1) → MvPolynomial (Fin (n + 1)) K} (hφ : IsProjectiveMorphism d φ) : ∃ (M : ℕ) (q : Fin (n + 1) × Fin (m + 1) → MvPolynomial (Fin (n + 1)) K), (∀ (a : Fin (n + 1) × Fin (m + 1)), (q a).IsHomogeneous M) ∧ ∀ (x : Fin (n + 1) → K) (k : Fin (n + 1)), ∑ j : Fin (m + 1), (MvPolynomial.eval x) (q (k, j)) * (MvPolynomial.eval x) (φ j) = x k ^ (M + d)

theorem theorem_25_14_upper_bound {K : Type u_1} [Field K] [NumberField K] {n m d : ℕ} {φ : Fin (m + 1) → MvPolynomial (Fin (n + 1)) K} (hφ : IsProjectiveMorphism d φ) : ∃ (C₁ : ℝ), ∀ (x : Fin (n + 1) → K), (Height.logHeight fun (j : Fin (m + 1)) => (MvPolynomial.eval x) (φ j)) ≤ C₁ + ↑d * Height.logHeight x

theorem theorem_25_14_lower_bound {K : Type u_1} [Field K] [NumberField K] {n m d : ℕ} {φ : Fin (m + 1) → MvPolynomial (Fin (n + 1)) K} (hφ : IsProjectiveMorphism d φ) : ∃ (C₂ : ℝ), ∀ (x : Fin (n + 1) → K), C₂ + ↑d * Height.logHeight x ≤ Height.logHeight fun (j : Fin (m + 1)) => (MvPolynomial.eval x) (φ j)

theorem theorem_25_14_combined {K : Type u_1} [Field K] [NumberField K] {n m d : ℕ} {φ : Fin (m + 1) → MvPolynomial (Fin (n + 1)) K} (hφ : IsProjectiveMorphism d φ) : ∃ (C : ℝ), ∀ (x : Fin (n + 1) → K), |(Height.logHeight fun (j : Fin (m + 1)) => (MvPolynomial.eval x) (φ j)) - ↑d * Height.logHeight x| ≤ C