mathlib3

550b5853 - chore(algebraic_geometry/elliptic_curve/weierstrass): add disclaimer for coordinate_ring irreducibility (#17977)

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]`. Co-authored-by: Anne Baanen <t.baanen@vu.nl>