Theorems · Theorem · algebraic geometry

WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis

∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (p q : Polynomial R),
  (Algebra.norm (Polynomial R)) (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X) =
    p ^ 2 - p * q * (Polynomial.C W'.a₁ * Polynomial.X + Polynomial.C W'.a₃) -
      q ^ 2 *
        (Polynomial.X ^ 3 + Polynomial.C W'.a₂ * Polynomial.X ^ 2 + Polynomial.C W'.a₄ * Polynomial.X +
          Polynomial.C W'.a₆)

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRing