Commit 2025-04-25 07:22 11cedf3d

View on Github →

chore(AlgebraicGeometry/EllipticCurve/*): refactor VariableChange (#23217) Drop certain definitions in VariableChange in favor of mathlib's built-in notation:

VariableChange.id -> (1 : VariableChange R)
VariableChange.comp C C' -> C * C'
VariableChange.inv C -> C⁻¹
W.variableChange C -> C • W

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean

modified theorem WeierstrassCurve.exists_variableChange_of_j_eq

Modified Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean

modified theorem WeierstrassCurve.exists_variableChange_isCharNeTwoNF

modified theorem WeierstrassCurve.exists_variableChange_isCharThreeNF

modified theorem WeierstrassCurve.exists_variableChange_isCharTwoNF

modified theorem WeierstrassCurve.exists_variableChange_isShortNF

modified theorem WeierstrassCurve.toCharThreeNF_spec_of_b₂_eq_zero

modified theorem WeierstrassCurve.toShortNFOfCharThree_a₂

modified theorem WeierstrassCurve.toShortNFOfCharThree_spec

Modified Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean

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

added theorem WeierstrassCurve.VariableChange.inv_def

added theorem WeierstrassCurve.VariableChange.mul_def

added theorem WeierstrassCurve.VariableChange.one_def

modified theorem WeierstrassCurve.coe_inv_variableChange_Δ'

modified theorem WeierstrassCurve.coe_variableChange_Δ'

modified theorem WeierstrassCurve.inv_variableChange_Δ'

modified theorem WeierstrassCurve.map_variableChange

deleted def WeierstrassCurve.variableChange

added theorem WeierstrassCurve.variableChange_a₁

added theorem WeierstrassCurve.variableChange_a₂

added theorem WeierstrassCurve.variableChange_a₃

added theorem WeierstrassCurve.variableChange_a₄

added theorem WeierstrassCurve.variableChange_a₆

modified theorem WeierstrassCurve.variableChange_b₂

modified theorem WeierstrassCurve.variableChange_b₄

modified theorem WeierstrassCurve.variableChange_b₆

modified theorem WeierstrassCurve.variableChange_b₈

deleted theorem WeierstrassCurve.variableChange_comp

modified theorem WeierstrassCurve.variableChange_c₄

modified theorem WeierstrassCurve.variableChange_c₆

added theorem WeierstrassCurve.variableChange_def

deleted theorem WeierstrassCurve.variableChange_id

modified theorem WeierstrassCurve.variableChange_j

modified theorem WeierstrassCurve.variableChange_Δ'

modified theorem WeierstrassCurve.variableChange_Δ