Commit 2022-12-19 16:43 550b5853

View on Github →

chore(algebraic_geometry/elliptic_curve/weierstrass): add disclaimer for coordinate_ring irreducibility (#17977) Also rename coe_inv lemmas to be consistent with those generated by @[simps].

Estimated changes

Modified src/algebraic_geometry/elliptic_curve/weierstrass.lean

deleted theorem elliptic_curve.coe_base_change_Δ'_inv

added theorem elliptic_curve.coe_inv_base_change_Δ'

added theorem elliptic_curve.coe_inv_variable_change_Δ'

deleted theorem elliptic_curve.coe_variable_change_Δ'_inv

deleted def weierstrass_curve.coordinate_ring