Theorems · Theorem · number theory

WeierstrassCurve.abs_logHeight_addSubMap_sub_two_mul_logHeight_le

∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (W : WeierstrassCurve K) [W.IsElliptic],
  ∃ C,
    ∀ (x : Fin 3 → K), |(Height.logHeight fun i => (MvPolynomial.eval x) (W.addSubMap i)) - 2 * Height.logHeight x| ≤ C

If W is a Weierstrass curve over K, then the map F : ℙ² → ℙ² given by addSubMap W is a morphism. This implies that |logHeight (F x) - 2 * logHeight x| ≤ C for a constant C, where x = ![s, t, u] and F acts on the coordinate vector.

Defined in

Mathlib.NumberTheory.Height.EllipticCurve

Cited by

0 results in Mathlib

Foundations

Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldHeight.AdmissibleAbsValuesWeierstrassCurve.IsElliptic