Theorems · Theorem · algebraic geometry
WeierstrassCurve.Projective.eval_polynomialX
∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R),
(MvPolynomial.eval P) W'.polynomialX = W'.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W'.a₂ * P 0 * P 2 + W'.a₄ * P 2 ^ 2)- Cited by
- 6 results in Mathlib
- Foundations
- Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- RingHomstatement · cited by 10,189
- Finsuppstatement · cited by 5,255
- MvPolynomialstatement and proof · cited by 2,140
- map_mulproof · cited by 1,137
- map_addproof · cited by 964
- map_subproof · cited by 565
- MvPolynomial.Xproof · cited by 552
- map_powproof · cited by 503
- MvPolynomial.Cproof · cited by 400
- WeierstrassCurve.a₁statement and proof · cited by 272
Cited by6
Results whose statement or proof uses this declaration.
- WeierstrassCurve.Projective.dblU_eqproof · cited by 3
- WeierstrassCurve.Projective.dblX_eq'proof · cited by 2
- WeierstrassCurve.Projective.negDblY_eq'proof · cited by 2
- WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zeroproof · cited by 1
- WeierstrassCurve.Projective.nonsingular_iffproof · cited by 1
- WeierstrassCurve.Projective.polynomial_relationproof · cited by 0