English
Relates the product of a smul-basis combination with Y to a combination of generators and Y with coefficients derived from the Weierstrass coefficients.
Русский
Связь произведения smul-组合 с Y с линейной комбинацией генераторов и Y с коэффициентами коэффициентами кривой Ваирачстраса.
LaTeX
$$(p • 1 + q • mk W' Y) * mk W' Y = q • (X^3 + a₂ X^2 + a₄ X + a₆) • 1 + (p - q • (a₁ X + a₃)) • mk W' Y$$
Lean4
theorem smul_basis_mul_Y (p q : R[X]) :
(p • (1 : W'.CoordinateRing) + q • mk W' Y) * mk W' Y =
(q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • (1 : W'.CoordinateRing) +
(p - q * (C W'.a₁ * X + C W'.a₃)) • mk W' Y :=
by
have Y_sq :
mk W' Y ^ 2 = mk W' (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) - C (C W'.a₁ * X + C W'.a₃) * Y) :=
AdjoinRoot.mk_eq_mk.mpr ⟨1, by rw [polynomial]; ring1⟩
simp only [smul, add_mul, mul_assoc, ← sq, Y_sq, map_sub, map_mul]
ring1