Theorems · Theorem · number theory

WeierstrassCurve.isIntegral_of_exists_lift

∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] {W : WeierstrassCurve K},
  (∃ r₁, (algebraMap R K) r₁ = W.a₁) →
    (∃ r₂, (algebraMap R K) r₂ = W.a₂) →
      (∃ r₃, (algebraMap R K) r₃ = W.a₃) →
        (∃ r₄, (algebraMap R K) r₄ = W.a₄) → (∃ r₆, (algebraMap R K) r₆ = W.a₆) → WeierstrassCurve.IsIntegral R W

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebra