Commit 2024-09-30 15:34 a6e5517e

View on Github →

chore(AlgebraicGeometry/EllipticCurve/*): split VariableChange into a new file (#17199)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

Created Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean

added theorem EllipticCurve.coe_inv_variableChange_Δ'

added theorem EllipticCurve.coe_variableChange_Δ'

added def EllipticCurve.variableChange

added theorem EllipticCurve.variableChange_comp

added theorem EllipticCurve.variableChange_id

added theorem EllipticCurve.variableChange_j

added def WeierstrassCurve.VariableChange.comp

added theorem WeierstrassCurve.VariableChange.comp_assoc

added theorem WeierstrassCurve.VariableChange.comp_id

added theorem WeierstrassCurve.VariableChange.comp_left_inv

added def WeierstrassCurve.VariableChange.id

added theorem WeierstrassCurve.VariableChange.id_comp

added def WeierstrassCurve.VariableChange.inv

added def WeierstrassCurve.VariableChange.map

added def WeierstrassCurve.VariableChange.mapHom

added theorem WeierstrassCurve.VariableChange.map_baseChange

added theorem WeierstrassCurve.VariableChange.map_id

added theorem WeierstrassCurve.VariableChange.map_injective

added theorem WeierstrassCurve.VariableChange.map_map

added structure WeierstrassCurve.VariableChange

added theorem WeierstrassCurve.map_variableChange

added def WeierstrassCurve.variableChange

added theorem WeierstrassCurve.variableChange_b₂

added theorem WeierstrassCurve.variableChange_b₄

added theorem WeierstrassCurve.variableChange_b₆

added theorem WeierstrassCurve.variableChange_b₈

added theorem WeierstrassCurve.variableChange_comp

added theorem WeierstrassCurve.variableChange_c₄

added theorem WeierstrassCurve.variableChange_c₆

added theorem WeierstrassCurve.variableChange_id

added theorem WeierstrassCurve.variableChange_Δ

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

deleted theorem EllipticCurve.coe_inv_variableChange_Δ'

deleted theorem EllipticCurve.coe_variableChange_Δ'

deleted def EllipticCurve.variableChange

deleted theorem EllipticCurve.variableChange_comp

deleted theorem EllipticCurve.variableChange_id

deleted theorem EllipticCurve.variableChange_j

deleted def WeierstrassCurve.VariableChange.comp

deleted theorem WeierstrassCurve.VariableChange.comp_assoc

deleted theorem WeierstrassCurve.VariableChange.comp_id

deleted theorem WeierstrassCurve.VariableChange.comp_left_inv

deleted def WeierstrassCurve.VariableChange.id

deleted theorem WeierstrassCurve.VariableChange.id_comp

deleted def WeierstrassCurve.VariableChange.inv

deleted def WeierstrassCurve.VariableChange.map

deleted def WeierstrassCurve.VariableChange.mapHom

deleted theorem WeierstrassCurve.VariableChange.map_baseChange

deleted theorem WeierstrassCurve.VariableChange.map_id

deleted theorem WeierstrassCurve.VariableChange.map_injective

deleted theorem WeierstrassCurve.VariableChange.map_map

deleted structure WeierstrassCurve.VariableChange

deleted theorem WeierstrassCurve.map_variableChange

deleted def WeierstrassCurve.variableChange

deleted theorem WeierstrassCurve.variableChange_b₂

deleted theorem WeierstrassCurve.variableChange_b₄

deleted theorem WeierstrassCurve.variableChange_b₆

deleted theorem WeierstrassCurve.variableChange_b₈

deleted theorem WeierstrassCurve.variableChange_comp

deleted theorem WeierstrassCurve.variableChange_c₄

deleted theorem WeierstrassCurve.variableChange_c₆

deleted theorem WeierstrassCurve.variableChange_id

deleted theorem WeierstrassCurve.variableChange_Δ