Commit 2024-12-23 16:10 00d6d7bb

View on Github →

feat(AlgebraicGeometry/EllipticCurve/Projective): add maps and base changes (#20022)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

added theorem MvPolynomial.eval₂_comp

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean

added theorem WeierstrassCurve.Projective.Equation.map

added theorem WeierstrassCurve.Projective.baseChange_add

added theorem WeierstrassCurve.Projective.baseChange_addX

added theorem WeierstrassCurve.Projective.baseChange_addXYZ

added theorem WeierstrassCurve.Projective.baseChange_addY

added theorem WeierstrassCurve.Projective.baseChange_dblU

added theorem WeierstrassCurve.Projective.baseChange_dblX

added theorem WeierstrassCurve.Projective.baseChange_dblXYZ

added theorem WeierstrassCurve.Projective.baseChange_dblY

added theorem WeierstrassCurve.Projective.baseChange_dblZ

added theorem WeierstrassCurve.Projective.baseChange_equation

added theorem WeierstrassCurve.Projective.baseChange_negAddY

added theorem WeierstrassCurve.Projective.baseChange_negDblY

added theorem WeierstrassCurve.Projective.baseChange_negY

added theorem WeierstrassCurve.Projective.baseChange_nonsingular

added theorem WeierstrassCurve.Projective.baseChange_polynomial

added theorem WeierstrassCurve.Projective.baseChange_polynomialX

added theorem WeierstrassCurve.Projective.baseChange_polynomialY

added theorem WeierstrassCurve.Projective.baseChange_polynomialZ

added theorem WeierstrassCurve.Projective.comp_equiv_comp

added theorem WeierstrassCurve.Projective.comp_smul

added theorem WeierstrassCurve.Projective.map_addU

added theorem WeierstrassCurve.Projective.map_addX

added theorem WeierstrassCurve.Projective.map_addXYZ

added theorem WeierstrassCurve.Projective.map_addY

added theorem WeierstrassCurve.Projective.map_addZ

added theorem WeierstrassCurve.Projective.map_dblU

added theorem WeierstrassCurve.Projective.map_dblX

added theorem WeierstrassCurve.Projective.map_dblXYZ

added theorem WeierstrassCurve.Projective.map_dblY

added theorem WeierstrassCurve.Projective.map_dblZ

added theorem WeierstrassCurve.Projective.map_equation

added theorem WeierstrassCurve.Projective.map_negAddY

added theorem WeierstrassCurve.Projective.map_negDblY

added theorem WeierstrassCurve.Projective.map_negY

added theorem WeierstrassCurve.Projective.map_nonsingular

added theorem WeierstrassCurve.Projective.map_polynomial

added theorem WeierstrassCurve.Projective.map_polynomialX

added theorem WeierstrassCurve.Projective.map_polynomialY

added theorem WeierstrassCurve.Projective.map_polynomialZ